English
If l1 ≤ l2, then l1.toFilter I ≤ l2.toFilter I for any I.
Русский
Если l1 ≤ l2, то l1.toFilter I ≤ l2.toFilter I для любого I.
LaTeX
$$$l_1 \\le l_2 \\Rightarrow l_1.toFilter I \\le l_2.toFilter I$$$
Lean4
theorem tendsto_embedBox_toFilteriUnion_top (l : IntegrationParams) (h : I ≤ J) :
Tendsto (TaggedPrepartition.embedBox I J h) (l.toFilteriUnion I ⊤)
(l.toFilteriUnion J (Prepartition.single J I h)) :=
by
simp only [toFilteriUnion, tendsto_iSup]; intro c
set π₀ := Prepartition.single J I h
refine le_iSup_of_le (max c π₀.compl.distortion) ?_
refine
((l.hasBasis_toFilterDistortioniUnion I c ⊤).tendsto_iff (l.hasBasis_toFilterDistortioniUnion J _ _)).2 fun r hr =>
?_
refine ⟨r, hr, fun π hπ => ?_⟩
rw [mem_setOf_eq, Prepartition.iUnion_top] at hπ
refine ⟨⟨hπ.1.1, hπ.1.2, fun hD => le_trans (hπ.1.3 hD) (le_max_left _ _), fun _ => ?_⟩, ?_⟩
· refine ⟨_, π₀.iUnion_compl.trans ?_, le_max_right _ _⟩
congr 1
exact (Prepartition.iUnion_single h).trans hπ.2.symm
· exact hπ.2.trans (Prepartition.iUnion_single _).symm
