norm_le_mul' — Mathlib

English

If h is Lipschitz with constant K and f(1)=1, then ∀ x, ∥f x∥ ≤ K ∥x∥.

Русский

Если h является липшицевым с константой K и f(1)=1, то для всех x выполняется ∥f x∥ ≤ K ∥x∥.

LaTeX

$$$\mathrm{LipschitzWith}(K,f) \land f(1)=1 \Rightarrow \forall x,\ \|f x\| ≤ K \|x\|.$$$

Lean4

@[to_additive LipschitzWith.norm_le_mul]
theorem norm_le_mul' {f : E → F} {K : ℝ≥0} (h : LipschitzWith K f) (hf : f 1 = 1) (x) : ‖f x‖ ≤ K * ‖x‖ := by
  simpa only [dist_one_right, hf] using h.dist_le_mul x 1

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