insert_empty — Mathlib

English

If s is a topological basis, then inserting the empty set yields a topological basis as well.

Русский

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

LaTeX

$$insert_empty {s : Set (Set α)} (h : IsTopologicalBasis s) : IsTopologicalBasis (insert ∅ s)$$

Lean4

theorem insert_empty {s : Set (Set α)} (h : IsTopologicalBasis s) : IsTopologicalBasis (insert ∅ s) :=
  h.of_isOpen_of_subset (by rintro _ (rfl | hu); exacts [isOpen_empty, h.isOpen hu]) (subset_insert ..)

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