lipschitzOnWith_univ — Mathlib

English

A function is Lipschitz on the whole space if and only if it is Lipschitz with respect to the global metric.

Русский

Функция липшицева на всей пространстве тогда и только тогда, когда она липшицева по глобальной метрике.

LaTeX

$$$LipschitzOnWith(K,f,univ)\ \iff\ LipschitzWith(K,f)$$$

Lean4

/-- `f` is Lipschitz iff it is Lipschitz on the entire space. -/
@[simp]
theorem lipschitzOnWith_univ : LipschitzOnWith K f univ ↔ LipschitzWith K f := by simp [LipschitzOnWith, LipschitzWith]

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