isUniformEmbedding — Mathlib

English

An isometry from an emetric space is a uniform embedding.

Русский

Изометрия из эмитрического пространства является равномерным вложением.

LaTeX

$$$Isometry(f) \rightarrow IsUniformEmbedding(f)$$$

Lean4

/-- An isometry from an emetric space is a uniform embedding -/
theorem isUniformEmbedding (hf : Isometry f) : IsUniformEmbedding f :=
  hf.antilipschitz.isUniformEmbedding hf.lipschitz.uniformContinuous

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