Theorems · Theorem · order theory

Filter.HasBasis.liminf_eq_sSup_iUnion_iInter

∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {ι : Type u_6} {ι' : Type u_7} {f : ι → α} {v : Filter ι}
  {p : ι' → Prop} {s : ι' → Set ι}, v.HasBasis p s → Filter.liminf f v = sSup (⋃ j, ⋂ i, Set.Iic (f ↑i))

Defined in

Mathlib.Order.LiminfLimsup

Cited by

4 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLattice