isTopologicalBasis — Mathlib

English

The family lowerBasis(α) forms a topological basis for the lower topology on α.

Русский

Семейство lowerBasis(α) образует топологический базис для нижней топологии на α.

LaTeX

$$$\\text{IsTopologicalBasis}(\\text{lowerBasis}(\\alpha))$$$

Lean4

protected theorem isTopologicalBasis : IsTopologicalBasis (lowerBasis α) :=
  by
  convert isTopologicalBasis_of_subbasis (topology_eq α)
  simp_rw [lowerBasis, coe_upperClosure, compl_iUnion]
  ext s
  constructor
  · rintro ⟨F, hF, rfl⟩
    refine ⟨(fun a => (Ici a)ᶜ) '' F, ⟨hF.image _, image_subset_iff.2 fun _ _ => ⟨_, rfl⟩⟩, ?_⟩
    simp only [sInter_image]
  · rintro ⟨F, ⟨hF, hs⟩, rfl⟩
    haveI := hF.to_subtype
    rw [subset_def, Subtype.forall'] at hs
    choose f hf using hs
    exact ⟨_, finite_range f, by simp_rw [biInter_range, hf, sInter_eq_iInter]⟩

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