isTopologicalBasis_Iic_principal — Mathlib

English

The range of Set.Iic ∘ Filter.principal is a topological basis.

Русский

Область диапазона Set.Iic ∘ Filter.principal образует топологическую базису.

LaTeX

$$$$\text{IsTopologicalBasis}(\text{range}(\mathrm{Iic}\circ \mathrm{principal})).$$$$

Lean4

theorem isTopologicalBasis_Iic_principal : IsTopologicalBasis (range (Iic ∘ 𝓟 : Set α → Set (Filter α))) :=
  { exists_subset_inter := by
      rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩ l hl
      exact ⟨Iic (𝓟 s) ∩ Iic (𝓟 t), ⟨s ∩ t, by simp⟩, hl, Subset.rfl⟩
    sUnion_eq := sUnion_eq_univ_iff.2 fun _ => ⟨Iic ⊤, ⟨univ, congr_arg Iic principal_univ⟩, mem_Iic.2 le_top⟩
    eq_generateFrom := rfl }

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