le_mul_norm' — Mathlib

English

If h is AntilipschitzWith K and f(1)=1, then ∀ x, ∥x∥ ≤ K ∥f x∥ in NNNorm sense.

Русский

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

LaTeX

$$$\left( h: \mathrm{AntilipschitzWith}~K~f \right) \Rightarrow \forall x,\ \|x\| ≤ K \|f x\|,$$$

Lean4

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

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