nnorm_le_mul' — Mathlib

English

If h is Lipschitz with NNReal constant K and f maps to NNNorm, then ∥f x∥ ≤ K ∥x∥ in NNNorm sense.

Русский

Если LipschitzWith с константой NNReal K и отображение в NNNorm, то ∥f x∥ ≤ K ∥x∥ в смысле nnorm.

LaTeX

$$$\forall x,\ \|f x\|_{nn} \le K \|x\|_{nn}. $$$

Lean4

@[to_additive LipschitzWith.nnorm_le_mul]
theorem nnorm_le_mul' {f : E → F} {K : ℝ≥0} (h : LipschitzWith K f) (hf : f 1 = 1) (x) : ‖f x‖₊ ≤ K * ‖x‖₊ :=
  h.norm_le_mul' hf x

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