isometry — Mathlib

English

The Kuratowski embedding is an isometry.

Русский

Встраивание Куротовского является изометрией.

LaTeX

$$$\text{Isometry}(\text{kuratowskiEmbedding } \alpha)$$$

Lean4

/-- The Kuratowski embedding is an isometry.
Theorem 2.1 of [Assaf Naor, *Metric Embeddings and Lipschitz Extensions*][Naor-2015]. -/
protected theorem isometry (α : Type u) [MetricSpace α] [SeparableSpace α] : Isometry (kuratowskiEmbedding α) :=
  Classical.choose_spec (exists_isometric_embedding α)

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