le_mul_nnnorm' — Mathlib

English

If f is an isometry and f(1)=1, then ∥f x∥₊ = ∥x∥₊ for all x.

Русский

Если f изометрия и f(1)=1, то ∥f x∥₊ = ∥x∥₊ для всех x.

LaTeX

$$$\mathrm{Isometry}(f) \Rightarrow \forall x,\ \|f x\|_{+} = \|x\|_{+}.$$$

Lean4

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

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