toFilterDistortioniUnion_neBot — Mathlib

English

If distortions on π0 bounds hold, then the filtered union l.toFilterDistortioniUnion I c π0 is nonempty.

Русский

Если ограничение искажений на π0 выполняется, фильтр DistortioniUnion I c π0 не пуст.

LaTeX

$$$(l.toFilterDistortioniUnion I c π_0).NeBot$$$

Lean4

theorem toFilterDistortioniUnion_neBot (l : IntegrationParams) (I : Box ι) (π₀ : Prepartition I)
    (hc₁ : π₀.distortion ≤ c) (hc₂ : π₀.compl.distortion ≤ c) : (l.toFilterDistortioniUnion I c π₀).NeBot :=
  ((l.hasBasis_toFilterDistortion I _).inf_principal _).neBot_iff.2 fun {r} _ =>
    (l.exists_memBaseSet_le_iUnion_eq π₀ hc₁ hc₂ r).imp fun _ hπ => ⟨hπ.1, hπ.2.2⟩

Похожие утверждения