English
The filter (l.toFilteriUnion I π0) has a basis with the family of maps r ↦ (l.RCond (r c)) and the sets {π | ∃ c, MemBaseSet I c (r c) π ∧ π.iUnion = π0.iUnion}.
Русский
Фильтр (l.toFilteriUnion I π0) имеет базис с семейством отображений r ↦ (l.RCond (r c)) и множеством {π | ∃ c, MemBaseSet I c (r c) π ∧ π.iUnion = π0.iUnion}.
LaTeX
$$$(l.toFilteriUnion I \\pi_0).HasBasis (\\lambda r. l.RCond (r)) \\\\;{\\pi | \\exists c, l.MemBaseSet I c (r c) \\pi \\land \\pi.iUnion = \\pi_0.iUnion}$$$
Lean4
theorem hasBasis_toFilteriUnion (l : IntegrationParams) (I : Box ι) (π₀ : Prepartition I) :
(l.toFilteriUnion I π₀).HasBasis (fun r : ℝ≥0 → (ι → ℝ) → Ioi (0 : ℝ) => ∀ c, l.RCond (r c)) fun r =>
{π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.iUnion = π₀.iUnion} :=
by
have := fun c => l.hasBasis_toFilterDistortioniUnion I c π₀
simpa only [setOf_and, setOf_exists] using hasBasis_iSup this
