Theorems · Theorem · order theory

Filter.inf_liminf

∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {u : β → α} [f.NeBot] (a : α),
  a ⊓ Filter.liminf u f = Filter.liminf (fun x => a ⊓ u x) f

Defined in

Mathlib.Order.LiminfLimsup

Cited by

1 results in Mathlib

Foundations

Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CompleteDistribLatticeFilter.NeBot