English
A set s belongs to countableGenerate g iff there exists a countable subcollection of g whose intersection is contained in s.
Русский
Множество s принадлежит countableGenerate g тогда и только тогда, когда существует счетное подмножество g, пересечение которого содержится в s.
LaTeX
$$$s \\in countableGenerate g \\iff \\exists S \\subseteq g, S \\text{ Countable} \\wedge \\bigcap S \\subseteq s$$$
Lean4
/-- A set is in the `countableInterFilter` generated by `g` if and only if
it contains a countable intersection of elements of `g`. -/
theorem mem_countableGenerate_iff {s : Set α} :
s ∈ countableGenerate g ↔ ∃ S : Set (Set α), S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ s :=
by
constructor <;> intro h
·
induction h with
| @basic s hs => exact ⟨{ s }, by simp [hs, subset_refl]⟩
| univ => exact ⟨∅, by simp⟩
| superset _ _ ih => refine Exists.imp (fun S => ?_) ih; tauto
| @sInter S Sct _ ih =>
choose T Tg Tct hT using ih
refine ⟨⋃ (s) (H : s ∈ S), T s H, by simpa, Sct.biUnion Tct, ?_⟩
apply subset_sInter
intro s H
exact subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)
rcases h with ⟨S, Sg, Sct, hS⟩
refine mem_of_superset ((countable_sInter_mem Sct).mpr ?_) hS
intro s H
exact CountableGenerateSets.basic (Sg H)
