dist_le_two_norm — Mathlib

English

For any x,y ∈ α, the distance between f(x) and f(y) is at most 2‖f‖: dist(f(x), f(y)) ≤ 2‖f‖.

Русский

Для любых x,y ∈ α расстояние между f(x) и f(y) не превышает 2‖f‖: dist(f(x), f(y)) ≤ 2‖f‖.

LaTeX

$$$\operatorname{dist}(f(x), f(y)) \le 2 \|f\| \quad (x,y \in \alpha)$$$

Lean4

/-- Distance between the images of any two points is at most twice the norm of the function. -/
theorem dist_le_two_norm (x y : α) : dist (f x) (f y) ≤ 2 * ‖f‖ :=
  (mkOfCompact f).dist_le_two_norm x y

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