diam_image_le — Mathlib

English

If s is bounded and f is Lipschitz with constant K, then the diameter of the image is at most K times the diameter of s.

Русский

Пусть s ограничено и f Lipschitz с константой K. Тогда диаметр образа ≤ K·диаметр s.

LaTeX

$$$\\operatorname{IsBounded}(s) \\Rightarrow \\operatorname{diam}(f''s) \\le K \\cdot \\operatorname{diam}(s)$$$

Lean4

theorem diam_image_le (hf : LipschitzWith K f) (s : Set α) (hs : IsBounded s) :
    Metric.diam (f '' s) ≤ K * Metric.diam s :=
  Metric.diam_le_of_forall_dist_le (mul_nonneg K.coe_nonneg Metric.diam_nonneg) <|
    forall_mem_image.2 fun _x hx =>
      forall_mem_image.2 fun _y hy => hf.dist_le_mul_of_le <| Metric.dist_le_diam_of_mem hs hx hy

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