antilipschitzWith_mul_left — Mathlib

English

If a ≠ 0, left multiplication by a is antilipschitz with constant (‖a‖)⁻¹.

Русский

Если a ≠ 0, левоудвоение на a является антиплешком с константой 1/‖a‖.

LaTeX

$$$ a \\neq 0 \\Rightarrow \\text{AntilipschitzWith}(\\|a\\|^{-1}, x \\mapsto a x).$$$

Lean4

theorem antilipschitzWith_mul_left {a : α} (ha : a ≠ 0) : AntilipschitzWith (‖a‖₊⁻¹) (a * ·) :=
  AntilipschitzWith.of_le_mul_dist fun _ _ ↦ by simp [dist_eq_norm, ← mul_sub, ha]

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