toGHSpace_rep — Mathlib

English

For X, Y compact nonempty metric spaces, toGHSpace X = toGHSpace Y iff there exists an isometryEquiv X Y.

Русский

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

LaTeX

$$$\forall X Y,\ toGHSpace X = toGHSpace Y \iff (\exists e: X \simeqᵢ Y).$$$

Lean4

theorem toGHSpace_rep (p : GHSpace) : toGHSpace p.Rep = p :=
  by
  change toGHSpace (Quot.out p : NonemptyCompacts ℓ_infty_ℝ) = p
  rw [← eq_toGHSpace]
  exact Quot.out_eq p

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