isTopologicalBasis_of_subbasis_of_inter

English

If t = generateFrom r and r is closed under finite intersections, then insert univ r is a topological basis.

Русский

Если t = generateFrom r и r замкнуто по отношению к конечным пересечениям, то добавление всеобщности к r образует топологическую базу.

LaTeX

$$t = generateFrom r ∧ (∀ s,t ∈ r, s ∩ t ∈ r) ⇒ IsTopologicalBasis (insert univ r)$$

Lean4

theorem isTopologicalBasis_of_subbasis_of_inter {r : Set (Set α)} (hsg : t = generateFrom r)
    (hsi : ∀ ⦃s⦄, s ∈ r → ∀ ⦃t⦄, t ∈ r → s ∩ t ∈ r) : IsTopologicalBasis (insert univ r) :=
  isTopologicalBasis_of_subbasis_of_finiteInter (by simpa using hsg) (FiniteInter.mk₂ hsi)

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