eq_toGHSpace — Mathlib

English

Two nonempty compact metric spaces X and Y have the same GHSpace image if and only if they are isometric; equivalently, there exists an isometry between X and Y.

Русский

Две непустые компактные метрические пространства X и Y имеют одинаковое изображение в GHSpace тогда и только тогда, когда они изометричны; то есть существует изометрия между X и Y.

LaTeX

$$$toGHSpace(X) = toGHSpace(Y) \iff (\exists \, e: X \cong Y).$$$

Lean4

theorem eq_toGHSpace {p : NonemptyCompacts ℓ_infty_ℝ} : ⟦p⟧ = toGHSpace p :=
  eq_toGHSpace_iff.2 ⟨fun x => x, isometry_subtype_coe, Subtype.range_coe⟩

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