ediam_image_inter_le_of_le — Mathlib

English

For s, t subsets, the image diameter of the intersection is bounded by the Holder constant times the diameter of the intersection, with a power r.

Русский

Для множеств s и t расстояние образа пересечения ограничено константой Холедера умноженной на диаметр пересечения возведённый в степень r.

LaTeX

$$$\\text{HolderOnWith } C r f s \\Rightarrow t \\subseteq s \\Rightarrow \\operatorname{diam}(f''(t \\cap s)) ≤ (C) * \\operatorname{diam}(t ∩ s)^{r}$$$

Lean4

theorem ediam_image_inter_le_of_le (hf : HolderOnWith C r f s) {d : ℝ≥0∞} (hd : EMetric.diam t ≤ d) :
    EMetric.diam (f '' (t ∩ s)) ≤ (C : ℝ≥0∞) * d ^ (r : ℝ) :=
  hf.ediam_image_le_of_subset_of_le inter_subset_right <| (EMetric.diam_mono inter_subset_left).trans hd

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