English
Given I, π0, distortion bounds hc1 and hc2 on π0 and its complement, and a function r, there exists a base set π with MemBaseSet I c r π and π.toPrepartition ≤ π0 with π.iUnion = π0.iUnion.
Русский
При заданных I, π0, ограничениях искажений hc1, hc2 и функции r существует база π с MemBaseSet I c r π и π.toPrepartition ≤ π0 и π.iUnion = π0.iUnion.
LaTeX
$$$\\exists \\pi, l.MemBaseSet I c r \\pi \\land \\pi.toPrepartition \\le π_0 ∧ π.iUnion = π_0.iUnion$$$
Lean4
theorem exists_memBaseSet_le_iUnion_eq (l : IntegrationParams) (π₀ : Prepartition I) (hc₁ : π₀.distortion ≤ c)
(hc₂ : π₀.compl.distortion ≤ c) (r : (ι → ℝ) → Ioi (0 : ℝ)) :
∃ π, l.MemBaseSet I c r π ∧ π.toPrepartition ≤ π₀ ∧ π.iUnion = π₀.iUnion :=
by
rcases π₀.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq r with ⟨π, hle, hH, hr, hd, hU⟩
refine ⟨π, ⟨hr, fun _ => hH, fun _ => hd.trans_le hc₁, fun _ => ⟨π₀.compl, ?_, hc₂⟩⟩, ⟨hle, hU⟩⟩
exact Prepartition.compl_congr hU ▸ π.toPrepartition.iUnion_compl
