toSubordinate_toPrepartition_le — Mathlib

English

The prepartition underlying π.toSubordinate r is a refinement of π, i.e., (π.toSubordinate r).toPrepartition ≤ π.

Русский

Предразбиение, лежащее в основе π.toSubordinate r, является разбиением более подробным, то есть (π.toSubordinate r).toPrepartition ≤ π.

LaTeX

$$$ (\\pi.toSubordinate r).toPrepartition \\le \\pi $$$

Lean4

theorem toSubordinate_toPrepartition_le (π : Prepartition I) (r : (ι → ℝ) → Ioi (0 : ℝ)) :
    (π.toSubordinate r).toPrepartition ≤ π :=
  (π.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq r).choose_spec.1

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