lipschitz_of_bound_nnnorm — Mathlib

English

Let f be a homomorphism and C ≥ 0. If ∀ x, ∥f x∥₊ ≤ C ∥x∥₊, then f is Lipschitz with constant C.

Русский

Пусть f — гомоморфизм и C ≥ 0. Если для всех x выполняется ∥f x∥₊ ≤ C ∥x∥₊, то f является липшицевым с константой C.

LaTeX

$$$\left( \forall x, \|f x\|_{+} \le C \cdot \|x\|_{+} \right) \Rightarrow \mathrm{LipschitzWith}(C,f).$$$

Lean4

@[to_additive]
theorem lipschitz_of_bound_nnnorm [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ≥0) (h : ∀ x, ‖f x‖₊ ≤ C * ‖x‖₊) :
    LipschitzWith C f :=
  @Real.toNNReal_coe C ▸ MonoidHomClass.lipschitz_of_bound f C h

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