sUnion_insert — Mathlib

English

Let s be a subset of α and T a collection of subsets of α. The union over insert s T equals s ∪ ⋃₀T: ⋃₀ insert s T = s ∪ ⋃₀T.

Русский

Пусть s ⊆ α и T — коллекция подмножеств α. Объединение над вставкой s в T равно s ∪ ⋃₀T: ⋃₀ insert s T = s ∪ ⋃₀T.

LaTeX

$$$$ \\bigcup_{U \\in \\mathrm{insert}(s,T)} U = s \\cup \\big( \\bigcup_{V \\in T} V \\big). $$$$

Lean4

@[simp]
theorem sUnion_insert (s : Set α) (T : Set (Set α)) : ⋃₀ insert s T = s ∪ ⋃₀ T :=
  sSup_insert

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