disjUnion_eq_union — Mathlib

English

If S and T are disjoint finite subsets of α, then their disjoint union equals their ordinary union.

Русский

Если два конечных подмножества S и T относительно α не пересекаются, то их дизъюнкционное объединение равно их обычному объединению.

LaTeX

$$$$ \text{Disjoint}(S,T) \quad \Rightarrow \quad S \uplus T = S \cup T, $$$$

Lean4

@[simp]
theorem disjUnion_eq_union (s t h) : @disjUnion α s t h = s ∪ t := by grind

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