hasBasis_generate — Mathlib

English

The smallest filter basis containing a family s is generated by finite intersections of members of s; i.e., sets are ⋂t over finite t ⊆ s.

Русский

Наименьший базис фильтра, содержащий семейство s, получается как конечные пересечения элементов s: множества вида ⋂ t, где t — конечное подмножество s.

LaTeX

$$$$ \text{The basis is } \{ \bigcap_{u \in t} u \mid t \text{ finite}, t \subseteq s \}. $$$$

Lean4

theorem hasBasis_generate (s : Set (Set α)) : (generate s).HasBasis (fun t => Set.Finite t ∧ t ⊆ s) fun t => ⋂₀ t :=
  ⟨fun U => by simp only [mem_generate_iff, and_assoc, and_left_comm]⟩

Похожие утверждения