English
Let S be a family of subsets of α. The filter generated by S consists precisely of those sets U that contain a finite intersection of members of S. Equivalently, U belongs to the generated filter generated by S if and only if there exists a finite subfamily t ⊆ S such that the intersection of all members of t is contained in U.
Русский
Пусть S — семейство подмножеств α. Фильтр, порождаемый S, состоит точно из тех множеств U, которые содержат конечное пересечение элементов S. Эквивалентно: U ∈ генерируемый фильтр S тогда и только тогда, существует конечное подсемейство t ⊆ S такое, что ⋂ t ⊆ U.
LaTeX
$$$ U \in \mathrm{generate}(s) \iff \exists t \subseteq s,\; \mathrm{Fin}(t) \land \bigcap_{V \in t} V \subseteq U $$
Lean4
theorem mem_generate_iff {s : Set <| Set α} {U : Set α} : U ∈ generate s ↔ ∃ t ⊆ s, Set.Finite t ∧ ⋂₀ t ⊆ U :=
by
constructor <;> intro h
·
induction h with
| @basic V V_in => exact ⟨{ V }, singleton_subset_iff.2 V_in, finite_singleton _, (sInter_singleton _).subset⟩
| univ => exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩
| superset _ hVW hV =>
rcases hV with ⟨t, hts, ht, htV⟩
exact ⟨t, hts, ht, htV.trans hVW⟩
| inter _ _ hV hW =>
rcases hV, hW with ⟨⟨t, hts, ht, htV⟩, u, hus, hu, huW⟩
exact ⟨t ∪ u, union_subset hts hus, ht.union hu, (sInter_union _ _).subset.trans <| inter_subset_inter htV huW⟩
· rcases h with ⟨t, hts, tfin, h⟩
exact mem_of_superset ((sInter_mem tfin).2 fun V hV => GenerateSets.basic <| hts hV) h
