English
Assume MemBaseSet holds for π1 and π2 with respect to c, r1 and r2, and that the iUnions are complementary to π1.iUnion. Then the union-complement operation yields a new base set under l with distortion controlled by c.
Русский
Предположим, что MemBaseSet выполняется для π1 и π2 относительно c, r1 и r2, и что iUnion дополняет π1.iUnion. Тогда операция unionComplToSubordinate порождает новую базовую координату под управлением l с ограничением искажения.
LaTeX
$$$\\forall \\pi_1, \\pi_2,\\, h_π: l.MemBaseSet I c r_1 \\pi_1,\\; (hle: \\forall x\\in I, r_2(x) \\le r_1(x))\\; \\forall (hU: \\pi_2.iUnion = I \\setminus \\pi_1.iUnion),\\; (hc: l.bDistortion \\rightarrow \\pi_2.distortion \\le c)\\; \\Rightarrow\\; l.MemBaseSet I c r_1 (\\pi_1.unionComplToSubordinate \\pi_2 hU r_2).$$$
Lean4
protected theorem unionComplToSubordinate (hπ₁ : l.MemBaseSet I c r₁ π₁) (hle : ∀ x ∈ Box.Icc I, r₂ x ≤ r₁ x)
{π₂ : Prepartition I} (hU : π₂.iUnion = ↑I \ π₁.iUnion) (hc : l.bDistortion → π₂.distortion ≤ c) :
l.MemBaseSet I c r₁ (π₁.unionComplToSubordinate π₂ hU r₂) :=
⟨hπ₁.1.disjUnion ((π₂.isSubordinate_toSubordinate r₂).mono hle) _, fun h =>
(hπ₁.2 h).disjUnion (π₂.isHenstock_toSubordinate _) _, fun h =>
(distortion_unionComplToSubordinate _ _ _ _).trans_le (max_le (hπ₁.3 h) (hc h)), fun _ => ⟨⊥, by simp⟩⟩
