isClosedEmbedding — Mathlib

English

A dilation from a complete emetric space is a closed embedding.

Русский

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

LaTeX

$$$\\text{IsClosedEmbedding}(f)$$$

Lean4

/-- A dilation from a complete emetric space is a closed embedding -/
theorem isClosedEmbedding [CompleteSpace α] [EMetricSpace β] [DilationClass F α β] (f : F) : IsClosedEmbedding f :=
  (antilipschitz f).isClosedEmbedding (lipschitz f).uniformContinuous

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