ediam_image_le — Mathlib

English

If f is LipschitzWith K f, then f is LipschitzOnWith K f on any subset s.

Русский

Если f липшицева с константой K, то она липшицева на любом подмножестве s.

LaTeX

$$$LipschitzWith(K,f)\Rightarrow LipschitzOnWith(K,f,s)$$$

Lean4

theorem ediam_image_le (hf : LipschitzWith K f) (s : Set α) : EMetric.diam (f '' s) ≤ K * EMetric.diam s :=
  by
  apply EMetric.diam_le
  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩
  exact hf.edist_le_mul_of_le (EMetric.edist_le_diam_of_mem hx hy)

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