generateFrom_insert_empty — Mathlib

English

Adding the empty set to a generating family does not change the generated sigma-algebra.

Русский

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

LaTeX

$$$\\text{generateFrom} (\\operatorname{insert} (\\emptyset) S) = \\text{generateFrom} S$$$

Lean4

@[simp]
theorem generateFrom_insert_empty (S : Set (Set α)) : generateFrom (insert ∅ S) = generateFrom S := by
  rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_empty, bot_sup_eq]

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