of_isOpen_of_subset — Mathlib

English

If s is a topological basis and s ⊆ s', and every element of s' is open, then s' is also a topological basis.

Русский

Если s является топологической базой и s ⊆ s', и каждый элемент s' открыт, то s' тоже является базой.

LaTeX

$$of_isOpen_of_subset {s s' : Set (Set α)} (h_open : ∀ u ∈ s', IsOpen u) (hs : IsTopologicalBasis s) (hss' : s ⊆ s') : IsTopologicalBasis s'$$

Lean4

theorem of_isOpen_of_subset {s s' : Set (Set α)} (h_open : ∀ u ∈ s', IsOpen u) (hs : IsTopologicalBasis s)
    (hss' : s ⊆ s') : IsTopologicalBasis s' :=
  isTopologicalBasis_of_isOpen_of_nhds h_open fun a _ ha u_open ↦
    have ⟨t, hts, ht⟩ := hs.isOpen_iff.mp u_open a ha;
    ⟨t, hss' hts, ht⟩

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