toFilterDistortioniUnion_neBot' — Mathlib

English

The NeBot property holds for the version with the maximum of distortions on π0.

Русский

Свойство NeBot сохраняется для варианта с максимумом искажений на π0.

LaTeX

$$$(l.toFilterDistortioniUnion I (\\max \\pi_0.distortion \\pi_0.compl.distortion) π_0).NeBot$$$

Lean4

instance toFilterDistortioniUnion_neBot' (l : IntegrationParams) (I : Box ι) (π₀ : Prepartition I) :
    (l.toFilterDistortioniUnion I (max π₀.distortion π₀.compl.distortion) π₀).NeBot :=
  l.toFilterDistortioniUnion_neBot I π₀ (le_max_left _ _) (le_max_right _ _)

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