locallyLipschitzOn_univ — Mathlib

English

A function is locally Lipschitz on the whole space if and only if it is locally Lipschitz as a function from the whole space.

Русский

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

LaTeX

$$$LocallyLipschitzOn(univ,f)\iff LocallyLipschitz(f)$$$

Lean4

@[simp]
theorem locallyLipschitzOn_univ : LocallyLipschitzOn univ f ↔ LocallyLipschitz f := by
  simp [LocallyLipschitzOn, LocallyLipschitz]

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