union_eq_iUnion — Mathlib

English

For sets s1 and s2, their union equals the iUnion over booleans of conditional selections: s1 ∪ s2 = ⋃ b : Bool, cond b s1 s2.

Русский

Для множеств s1 и s2 их объединение равно iUnion по булеву индексу: s1 ∪ s2 = ⋃ b : Bool, cond b s1 s2.

LaTeX

$$$$ s_{1} \\cup s_{2} = \\bigcup_{b : \\text{Bool}} \\operatorname{cond} (b)\\, s_{1}\\, s_{2}. $$$$

Lean4

theorem union_eq_iUnion {s₁ s₂ : Set α} : s₁ ∪ s₂ = ⋃ b : Bool, cond b s₁ s₂ :=
  sup_eq_iSup s₁ s₂

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