disjUnion_boxes — Mathlib

English

The boxes of the disjoint union equal the union of the boxes from both partitions, when the union is disjoint.

Русский

Коробки объединения без перекрытий равны объединению коробок из обоих разбиений, если объединение попарно непересекается.

LaTeX

$$$ (\pi_1.disjUnion\pi_2 h).boxes = π_1.boxes \cup π_2.boxes $$$

Lean4

@[simp]
theorem disjUnion_boxes (h : Disjoint π₁.iUnion π₂.iUnion) : (π₁.disjUnion π₂ h).boxes = π₁.boxes ∪ π₂.boxes :=
  rfl

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