sUnion_diff_singleton_empty — Mathlib

English

For any collection s of subsets of α, the union over s without the empty set equals the union over s: ⋃₀ (s \\ {∅}) = ⋃₀ s.

Русский

Для любой коллекции s подмножеств α объединение над s без пустого множества равно объединению над s: ⋃₀ (s \\ {∅}) = ⋃₀ s.

LaTeX

$$$$ \\bigcup_{U \\in s \\setminus \\{ \\emptyset \\}} U = \\bigcup_{U \\in s} U. $$$$

Lean4

@[simp]
theorem sUnion_diff_singleton_empty (s : Set (Set α)) : ⋃₀ (s \ {∅}) = ⋃₀ s :=
  sSup_diff_singleton_bot s

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