English
Let I be a box with finite index ι, and l an IntegrationParams. If l.MemBaseSet I c1 r1 π1 and l.MemBaseSet I c2 r2 π2 hold and the unions π1.iUnion and π2.iUnion are equal, then there exists a Prepartition π of I whose iUnion is the set-theoretic complement of π1.iUnion in I, and such that if distortion control by l is active then π.distortion is bounded by c1 and also by c2.
Русский
Пусть I — коробка над конечным индексом ι, а l — интеграционные параметры. Если выполняются условия MemBaseSet I c1 r1 π1 и MemBaseSet I c2 r2 π2 и объединения π1 и π2 совпадают, то существует предварительная партиция π такого, что π.iUnion = I \ π1.iUnion, и если применяется ограничение искажений, то dist π ≤ c1 и dist π ≤ c2.
LaTeX
$$$ \\exists \\pi: Prepartition I,\\; \\pi.iUnion = \\uparrow I \\setminus \\pi_1.iUnion\\; \\wedge\\; (l.bDistortion \\rightarrow \\pi.distortion \\le c_1) \\; \\wedge\\; (l.bDistortion \\rightarrow \\pi.distortion \\le c_2)$$$
Lean4
theorem exists_common_compl (h₁ : l.MemBaseSet I c₁ r₁ π₁) (h₂ : l.MemBaseSet I c₂ r₂ π₂) (hU : π₁.iUnion = π₂.iUnion) :
∃ π : Prepartition I,
π.iUnion = ↑I \ π₁.iUnion ∧ (l.bDistortion → π.distortion ≤ c₁) ∧ (l.bDistortion → π.distortion ≤ c₂) :=
by
wlog hc : c₁ ≤ c₂ with H
· simpa [hU, _root_.and_comm] using @H _ _ I c₂ c₁ l r₂ r₁ π₂ π₁ h₂ h₁ hU.symm (le_of_not_ge hc)
by_cases hD : (l.bDistortion : Prop)
· rcases h₁.4 hD with ⟨π, hπU, hπc⟩
exact ⟨π, hπU, fun _ => hπc, fun _ => hπc.trans hc⟩
· exact ⟨π₁.toPrepartition.compl, π₁.toPrepartition.iUnion_compl, fun h => (hD h).elim, fun h => (hD h).elim⟩
