English
Union of two tagged prepartitions with disjoint unions of boxes forms a new tagged prepartition whose boxes are the union of the two boxes, and whose tag is given by a piecewise combination.
Русский
Объединение двух помеченных предварительных разбиений с непересекающимися множествами коробок образует новое помеченное предварительное разбиение; коробки — это объединение двух множеств коробок; тег определяется по частям.
LaTeX
$$$ \text{disjUnion}(\pi_1,\pi_2,h) :\; (\text{toPrepartition} := \pi_1^{\text{toPrepartition}}.disjUnion\pi_2^{\text{toPrepartition}} h, \\n \text{tag} := \pi_1.boxes.piecewise(\pi_1.tag)(\pi_2.tag), \\n \dots $$$
Lean4
/-- Union of two tagged prepartitions with disjoint unions of boxes. -/
def disjUnion (π₁ π₂ : TaggedPrepartition I) (h : Disjoint π₁.iUnion π₂.iUnion) : TaggedPrepartition I
where
toPrepartition := π₁.toPrepartition.disjUnion π₂.toPrepartition h
tag := π₁.boxes.piecewise π₁.tag π₂.tag
tag_mem_Icc
J := by
dsimp only [Finset.piecewise]
split_ifs
exacts [π₁.tag_mem_Icc J, π₂.tag_mem_Icc J]
