iUnion_disjUnion — Mathlib

English

If h ensures π1.iUnion and π2.iUnion are disjoint, then the iUnion of π1.disjUnion π2 equals the union π1.iUnion ∪ π2.iUnion.

Русский

При условии, что iUnion π1 и iUnion π2 несовместны, iUnion от их объединения равняется объединению их iUnion.

LaTeX

$$$ (π_1.disjUnion π_2 h).iUnion = π_1.iUnion \cup π_2.iUnion. $$$

Lean4

@[simp]
theorem iUnion_disjUnion (h : Disjoint π₁.iUnion π₂.iUnion) : (π₁.disjUnion π₂ h).iUnion = π₁.iUnion ∪ π₂.iUnion := by
  simp [disjUnion, Prepartition.iUnion, iUnion_or, iUnion_union_distrib]

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