English
There is an eventual equality: for all t, π ⊓ splitMany I t equals (splitMany I t).filter J ⊆ π.iUnion.
Русский
Существует предельное равенство: для всех t выполняется π ⊓ splitMany I t = (splitMany I t).filter J ⊆ π.iUnion.
LaTeX
$$$\\forall t,\\ \\pi \\inf splitMany\\ I\\ t = (splitMany\\ I\\ t).filter(\\lambda J. J\\subseteq \\pi.iUnion)$$$
Lean4
theorem eventually_splitMany_inf_eq_filter (π : Prepartition I) :
∀ᶠ t : Finset (ι × ℝ) in atTop, π ⊓ splitMany I t = (splitMany I t).filter fun J => ↑J ⊆ π.iUnion :=
by
refine (eventually_not_disjoint_imp_le_of_mem_splitMany π.boxes).mono fun t ht => ?_
refine le_antisymm ((biUnion_le_iff _).2 fun J hJ => ?_) (le_inf (fun J hJ => ?_) (filter_le _ _))
· refine ofWithBot_mono ?_
simp only [Finset.mem_image, mem_boxes, mem_filter]
rintro _ ⟨J₁, h₁, rfl⟩ hne
refine ⟨_, ⟨J₁, ⟨h₁, Subset.trans ?_ (π.subset_iUnion hJ)⟩, rfl⟩, le_rfl⟩
exact ht I J hJ J₁ h₁ (mt disjoint_iff.1 hne)
· rw [mem_filter] at hJ
rcases Set.mem_iUnion₂.1 (hJ.2 J.upper_mem) with ⟨J', hJ', hmem⟩
refine ⟨J', hJ', ht I _ hJ' _ hJ.1 <| Box.not_disjoint_coe_iff_nonempty_inter.2 ?_⟩
exact ⟨J.upper, hmem, J.upper_mem⟩
