generateFrom_insert_empty — Mathlib

English

Adding the empty set to the generating family does not change the generated topology.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem generateFrom_insert_empty {α : Type*} {s : Set (Set α)} : generateFrom (insert ∅ s) = generateFrom s :=
  by
  rw [← sUnion_empty]
  exact generateFrom_insert_of_generateOpen (.sUnion ∅ (fun s_1 a ↦ False.elim a))

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