dist_le_two_norm' — Mathlib

English

If ∀ x, ‖f(x)‖ ≤ C, then ∀ x,y, dist (f(x)) (f(y)) ≤ 2C.

Русский

Если ∀ x, ‖f(x)‖ ≤ C, то ∀ x,y, dist (f(x)) (f(y)) ≤ 2C.

LaTeX

$$$\\forall x,y,\\ dist(f(x),f(y)) \\le 2C$ given $\\forall x, \\|f(x)\\| \\le C$$$

Lean4

theorem dist_le_two_norm' {f : γ → β} {C : ℝ} (hC : ∀ x, ‖f x‖ ≤ C) (x y : γ) : dist (f x) (f y) ≤ 2 * C :=
  calc
    dist (f x) (f y) ≤ ‖f x‖ + ‖f y‖ := dist_le_norm_add_norm _ _
    _ ≤ C + C := (add_le_add (hC x) (hC y))
    _ = 2 * C := (two_mul _).symm

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