generate_eq_biInf — Mathlib

English

For any S ⊆ Set α, the filter generated by S equals the infimum over s ∈ S of the principal filter generated by s.

Русский

Для любого S ⊆ Set α порожденный S фильтр равен наименьшей нижней границе над s ∈ S порождающих фильтров 𝓟 s.

LaTeX

$$$\mathrm{generate}(S) = \bigwedge_{s \in S} 𝓟 s$$

Lean4

theorem generate_eq_biInf (S : Set (Set α)) : generate S = ⨅ s ∈ S, 𝓟 s :=
  eq_of_forall_le_iff fun f => by simp [le_generate_iff, le_principal_iff, subset_def]

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