Theorems · Definition · general topology

Filter.ofCountableUnion

{α : Type u_2} →
  (l : Set (Set α)) →
    (∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l) → (∀ t ∈ l, ∀ s ⊆ t, s ∈ l) → Filter α

Construct a filter with countable intersection property. Similarly to Filter.comk, a set belongs to this filter if its complement satisfies the property. Similarly to Filter.ofCountableInter, this constructor deduces some properties from the countable intersection property which becomes the countable union property because we take complements of all sets.

Defined in

Mathlib.Order.Filter.CountableInter

Cited by

5 results in Mathlib

Foundations

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