English
If for every J in π, MemBaseSet J c r (πi J) holds and each πi J is a partition, then the tagged union π.biUnionTagged πi is a MemBaseSet for I with the same distortion bound c when l.bDistortion is assumed.
Русский
Если для каждого J в π выполняется MemBaseSet J c r (πi J) и каждый πi J является разбиением, то тегированное объединение π.biUnionTagged πi является MemBaseSet для I с тем же пределом искажений при условии l.bDistortion.
LaTeX
$$$\\forall J ∈ π,\\; l.MemBaseSet J c r (πi J)\\;\\wedge\\; \\forall J ∈ π, (πi J).IsPartition \\Rightarrow l.MemBaseSet I c r (π.biUnionTagged πi).$$$
Lean4
theorem biUnionTagged_memBaseSet {π : Prepartition I} {πi : ∀ J, TaggedPrepartition J}
(h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)) (hp : ∀ J ∈ π, (πi J).IsPartition)
(hc : l.bDistortion → π.compl.distortion ≤ c) : l.MemBaseSet I c r (π.biUnionTagged πi) :=
by
refine
⟨TaggedPrepartition.isSubordinate_biUnionTagged.2 fun J hJ => (h J hJ).1, fun hH =>
TaggedPrepartition.isHenstock_biUnionTagged.2 fun J hJ => (h J hJ).2 hH, fun hD => ?_, fun hD => ?_⟩
· rw [Prepartition.distortion_biUnionTagged, Finset.sup_le_iff]
exact fun J hJ => (h J hJ).3 hD
· refine ⟨_, ?_, hc hD⟩
rw [π.iUnion_compl, ← π.iUnion_biUnion_partition hp]
rfl
