antilipschitz_of_bound — Mathlib

English

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

Русский

Если f является AntilipschitzWith K и f(1)=1, то для всех x верно ∥x∥ ≤ K ∥f x∥.

LaTeX

$$$\left( f \text{ is AntilipschitzWith } K \text{ and } f(1)=1 \right) \Rightarrow \forall x,\ \|x\| \le K \|f x\|.$$$

Lean4

@[to_additive]
theorem antilipschitz_of_bound [MonoidHomClass 𝓕 E F] (f : 𝓕) {K : ℝ≥0} (h : ∀ x, ‖x‖ ≤ K * ‖f x‖) :
    AntilipschitzWith K f :=
  AntilipschitzWith.of_le_mul_dist fun x y => by simpa only [dist_eq_norm_div, map_div] using h (x / y)

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