English
For a given l, hunion, and hmono, s ∈ ofCountableUnion l hunion hmono iff l(s^c) holds.
Русский
Для заданных l, hunion и hmono, множество s принадлежит ofCountableUnion l hunion hmono тогда, когда выполнено соответствующее условие по complemento.
LaTeX
$$$s \\in Filter.ofCountableUnion l hunion hmono \\iff l(s^c)$$$
Lean4
/-- 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. -/
def ofCountableUnion (l : Set (Set α)) (hUnion : ∀ S : Set (Set α), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l)
(hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l) : Filter α :=
by
refine .ofCountableInter {s | sᶜ ∈ l} (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
· rw [mem_setOf_eq, compl_sInter]
apply hUnion (compl '' S) (hSc.image _)
intro s hs
rw [mem_image] at hs
rcases hs with ⟨t, ht, rfl⟩
apply hSp ht
· rw [mem_setOf_eq]
rw [← compl_subset_compl] at hsub
exact hmono sᶜ ht tᶜ hsub
