isClosedEmbedding — Mathlib

English

An isometry from a complete emetric space is a closed embedding.

Русский

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

LaTeX

$$$Isometry(f) \rightarrow IsClosedEmbedding(f)$$$

Lean4

/-- An isometry from a complete emetric space is a closed embedding -/
theorem isClosedEmbedding [CompleteSpace α] [EMetricSpace γ] {f : α → γ} (hf : Isometry f) : IsClosedEmbedding f :=
  hf.antilipschitz.isClosedEmbedding hf.lipschitz.uniformContinuous

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