ediam_image_le_of_subset — Mathlib

English

Same as above but with ENNReal bound on d.

Русский

То же самое, но с ограничением ENNReal на d.

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 (hf : HolderOnWith C r f s) (ht : t ⊆ s) :
    EMetric.diam (f '' t) ≤ (C : ℝ≥0∞) * EMetric.diam t ^ (r : ℝ) :=
  (hf.mono ht).ediam_image_le

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