English
Union of two disjoint prepartitions is a prepartition whose boxes are the union of the two box-collections; disjointness transfers to pairwise disjointness.
Русский
Объединение двух несовпадающих предразбиений образует предразбиение, чьи коробки являются объединением двух множеств коробок; несовместность сохраняется как парная несовместимость.
LaTeX
$$$(π_1 \ disjUnion π_2 h).boxes = π_1.boxes \cup π_2.boxes$$$
Lean4
/-- Union of two disjoint prepartitions. -/
@[simps]
def disjUnion (π₁ π₂ : Prepartition I) (h : Disjoint π₁.iUnion π₂.iUnion) : Prepartition I
where
boxes := π₁.boxes ∪ π₂.boxes
le_of_mem' _ hJ := (Finset.mem_union.1 hJ).elim π₁.le_of_mem π₂.le_of_mem
pairwiseDisjoint :=
suffices ∀ J₁ ∈ π₁, ∀ J₂ ∈ π₂, J₁ ≠ J₂ → Disjoint (J₁ : Set (ι → ℝ)) J₂ by
simpa [pairwise_union_of_symmetric (symmetric_disjoint.comap _), pairwiseDisjoint]
fun _ h₁ _ h₂ _ => h.mono (π₁.subset_iUnion h₁) (π₂.subset_iUnion h₂)
