toSubordinate — Mathlib

English

There is a subordinate tagged partition π' = π.toSubordinate r.

Русский

Существует тэгированное предразбиение π' = π.toSubordinate r, подчинённое функции r.

LaTeX

$$$ \\text{toSubordinate}(\\pi, r) \\text{ is a tagged partition subordinate to } r$$$

Lean4

/-- Given a prepartition `π` of a box `I` and a function `r : ℝⁿ → (0, ∞)`, `π.toSubordinate r`
is a tagged partition `π'` such that

* each box of `π'` is included in some box of `π`;
* `π'` is a Henstock partition;
* `π'` is subordinate to `r`;
* `π'` covers exactly the same part of `I` as `π`;
* the distortion of `π'` is equal to the distortion of `π`.
-/
def toSubordinate (π : Prepartition I) (r : (ι → ℝ) → Ioi (0 : ℝ)) : TaggedPrepartition I :=
  (π.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq r).choose

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