bound_of_antilipschitz — Mathlib

English

If f is an antilipschitz with constant K, then for all x, ∥x∥ ≤ K ∥f x∥.

Русский

Пусть f обладает свойством антилипшицевости с константой K; тогда для всех x выполняется ∥x∥ ≤ K ∥f x∥.

LaTeX

$$$\|x\| \le K \|f x\| \quad \text{for all } x.$$$

Lean4

@[to_additive]
theorem bound_of_antilipschitz [OneHomClass 𝓕 E F] (f : 𝓕) {K : ℝ≥0} (h : AntilipschitzWith K f) (x) :
    ‖x‖ ≤ K * ‖f x‖ :=
  h.le_mul_nnnorm' (map_one f) x

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