Theorems · Theorem · order theory

Filter.HasBasis.blimsup_eq_iInf_iSup

∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : CompleteLattice α] {p : ι → Prop} {s : ι → Set β} {f : Filter β}
  {u : β → α}, f.HasBasis p s → ∀ {q : β → Prop}, Filter.blimsup u f q = ⨅ i, ⨅ (_ : p i), ⨆ a ∈ s i, ⨆ (_ : q a), u a

Defined in

Mathlib.Order.LiminfLimsup

Cited by

2 results in Mathlib

Foundations

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

Assumes

CompleteLattice