of_edist_le — Mathlib

English

Locally Lipschitz on s f is equivalent to locally Lipschitz on the restricted function s.restrict f.

Русский

Локальная липшициевость на s f эквивалентна локальной липшициевости ограниченной функции s.restrict f.

LaTeX

$$$LocallyLipschitzOn(s,f)\iff LocallyLipschitz(s.restrict f)$$$

Lean4

protected theorem of_edist_le (h : ∀ x y, edist (f x) (f y) ≤ edist x y) : LipschitzWith 1 f := fun x y => by
  simp only [ENNReal.coe_one, one_mul, h]

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