generateFrom_insert_univ — Mathlib

English

Adding the universe to the generating family does not change the generated topology.

Русский

Добавление всего множества к порождающей семье не меняет порожденную топологию.

LaTeX

$$@[simp] theorem generateFrom_insert_univ {α : Type*} {s : Set (Set α)} : generateFrom (insert univ s) = generateFrom s$$

Lean4

@[simp]
theorem generateFrom_insert_univ {α : Type*} {s : Set (Set α)} : generateFrom (insert univ s) = generateFrom s :=
  generateFrom_insert_of_generateOpen .univ

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