English
If π is a MemBaseSet and p is any predicate on boxes, then the filtered prepartition π.filter p remains a MemBaseSet with the same c and r.
Русский
Если π удовлетворяет MemBaseSet и p — произвольное предикатное условие на коробки, то отфильтрованная предварительная партиция π.filter p сохраняет свой MemBaseSet с теми же параметрами c и r.
LaTeX
$$$ l.MemBaseSet I c r π \\rightarrow l.MemBaseSet I c r (π.filter p) $$$
Lean4
protected theorem filter (hπ : l.MemBaseSet I c r π) (p : Box ι → Prop) : l.MemBaseSet I c r (π.filter p) := by
classical
refine
⟨fun J hJ => hπ.1 J (π.mem_filter.1 hJ).1, fun hH J hJ => hπ.2 hH J (π.mem_filter.1 hJ).1, fun hD =>
(distortion_filter_le _ _).trans (hπ.3 hD), fun hD => ?_⟩
rcases hπ.4 hD with ⟨π₁, hπ₁U, hc⟩
set π₂ := π.filter fun J => ¬p J
have : Disjoint π₁.iUnion π₂.iUnion := by simpa [π₂, hπ₁U] using disjoint_sdiff_self_left.mono_right sdiff_le
refine ⟨π₁.disjUnion π₂.toPrepartition this, ?_, ?_⟩
· suffices ↑I \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion = ↑I \ (π.filter p).iUnion by simp [π₂, *]
have h : (π.filter p).iUnion ⊆ π.iUnion := biUnion_subset_biUnion_left (Finset.filter_subset _ _)
ext x
fconstructor
· rintro (⟨hxI, hxπ⟩ | ⟨hxπ, hxp⟩)
exacts [⟨hxI, mt (@h x) hxπ⟩, ⟨π.iUnion_subset hxπ, hxp⟩]
· rintro ⟨hxI, hxp⟩
by_cases hxπ : x ∈ π.iUnion
exacts [Or.inr ⟨hxπ, hxp⟩, Or.inl ⟨hxI, hxπ⟩]
· have : (π.filter fun J => ¬p J).distortion ≤ c := (distortion_filter_le _ _).trans (hπ.3 hD)
simpa [hc]
