ediam_image_le_of_subset_of_le — Mathlib

English

Variant of the previous bound for ENNReal bound on diameter.

Русский

Вариант предыдущего неравенства для другой размерности диаметра.

LaTeX

$$$\\text{HolderOnWith } C r f s \\Rightarrow t \\subseteq s \\Rightarrow \\forall d, ediam(t) ≤ d \\Rightarrow ediam(f''t) ≤ (C) * d^{r}$$$

Lean4

theorem ediam_image_le_of_subset_of_le (hf : HolderOnWith C r f s) (ht : t ⊆ s) {d : ℝ≥0∞} (hd : EMetric.diam t ≤ d) :
    EMetric.diam (f '' t) ≤ (C : ℝ≥0∞) * d ^ (r : ℝ) :=
  (hf.mono ht).ediam_image_le_of_le hd

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