lipschitz_evalx — Mathlib

English

For any x ∈ α, the map f ↦ f(x) is 1-Lipschitz: dist (f x) (g x) ≤ dist f g.

Русский

Для каждого x ∈ α отображение f ↦ f(x) является 1-Липшицевым: dist (f x) (g x) ≤ dist f g.

LaTeX

$$$\\forall x \\in α,\\; \\operatorname{dist}(f(x), g(x)) \\le \\operatorname{dist}(f, g).$$$

Lean4

theorem lipschitz_evalx (x : α) : LipschitzWith 1 fun f : α →ᵇ β => f x :=
  LipschitzWith.mk_one fun _ _ => dist_coe_le_dist x

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