English
Given a family l of sets of subsets of α, together with a rule for countable intersections and a monotonicity condition, we obtain a filter on α whose countable intersection property holds.
Русский
Пусть дано множество подмножеств α и правила счётной пересечения и монотонности; тогда образующий фильтр обладает свойством счетного пересечения.
LaTeX
$$$\\text{ofCountableInter}(l, hl, h_mono) : Filter α$$$
Lean4
/-- Construct a filter with countable intersection property. This constructor deduces
`Filter.univ_sets` and `Filter.inter_sets` from the countable intersection property. -/
def ofCountableInter (l : Set (Set α)) (hl : ∀ S : Set (Set α), S.Countable → S ⊆ l → ⋂₀ S ∈ l)
(h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) : Filter α
where
sets := l
univ_sets := @sInter_empty α ▸ hl _ countable_empty (empty_subset _)
sets_of_superset := h_mono _ _
inter_sets {s t} hs
ht :=
sInter_pair s t ▸ hl _ ((countable_singleton _).insert _) (insert_subset_iff.2 ⟨hs, singleton_subset_iff.2 ht⟩)
