id — Mathlib · SciLib

English

Let X be a pseudo-emetric space. The identity map id: X → X is 1-Lipschitz.

Русский

Пусть X — псевдоэммётрическое пространство. Отображение тождественноe id: X → X является 1‑липшицевым.

LaTeX

$$$\\operatorname{edist}(\\operatorname{id}\\,x, \\operatorname{id}\\,y) \\le 1 \\cdot \\operatorname{edist}(x,y)$$$

Lean4

/-- The identity is 1-Lipschitz. -/
protected theorem id : LipschitzWith 1 (@id α) :=
  LipschitzWith.of_edist_le fun _ _ => le_rfl

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