antilipschitzWith_mul_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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