isTopologicalBasis_of_subbasis_of_finiteInter

English

If a topology t equals the generateFrom of s and s is closed under finite intersections, then s is a topological basis.

Русский

Если топология t порождается генерацией generateFrom от s и s закрыта относительно конечных пересечений, то s является топологической базой.

LaTeX

$$isTopologicalBasis_of_subbasis_of_finiteInter {s : Set (Set α)} (hsg : t = generateFrom s) (hsi : FiniteInter s) : IsTopologicalBasis s$$

Lean4

theorem isTopologicalBasis_of_subbasis_of_finiteInter {s : Set (Set α)} (hsg : t = generateFrom s)
    (hsi : FiniteInter s) : IsTopologicalBasis s :=
  by
  convert isTopologicalBasis_of_subbasis hsg
  refine le_antisymm (fun t ht ↦ ⟨{ t }, by simpa using ht⟩) ?_
  rintro _ ⟨g, ⟨hg, hgs⟩, rfl⟩
  lift g to Finset (Set α) using hg
  exact hsi.finiteInter_mem g hgs

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