English
If π1 is a TaggedPrepartition and π2 is a Prepartition with hU describing π2.iUnion relative to I, then π1.unionComplToSubordinate π2 hU r is a partition.
Русский
Если π1 — тэгированное предразбиение, а π2 — предразбиение с описанием hU для iUnion, то π1.unionComplToSubordinate π2 hU r является разбиением.
LaTeX
$$$ \\mathrm{IsPartition}(\\pi_1.\\mathrm{unionComplToSubordinate}(\\pi_2,hU,r)) $$$
Lean4
/-- Given a tagged prepartition `π₁`, a prepartition `π₂` that covers exactly `I \ π₁.iUnion`, and
a function `r : ℝⁿ → (0, ∞)`, returns the union of `π₁` and `π₂.toSubordinate r`. This partition
`π` has the following properties:
* `π` is a partition, i.e. it covers the whole `I`;
* `π₁.boxes ⊆ π.boxes`;
* `π.tag J = π₁.tag J` whenever `J ∈ π₁`;
* `π` is Henstock outside of `π₁`: `π.tag J ∈ J.Icc` whenever `J ∈ π`, `J ∉ π₁`;
* `π` is subordinate to `r` outside of `π₁`;
* the distortion of `π` is equal to the maximum of the distortions of `π₁` and `π₂`.
-/
def unionComplToSubordinate (π₁ : TaggedPrepartition I) (π₂ : Prepartition I) (hU : π₂.iUnion = ↑I \ π₁.iUnion)
(r : (ι → ℝ) → Ioi (0 : ℝ)) : TaggedPrepartition I :=
π₁.disjUnion (π₂.toSubordinate r) (((π₂.iUnion_toSubordinate r).trans hU).symm ▸ disjoint_sdiff_self_right)
