English
There exist isometric embeddings Φ, Ψ into ℓ∞(ℝ) such that ghDist X Y equals the Hausdorff distance between the ranges of Φ and Ψ.
Русский
Существуют изометрические вложения Φ, Ψ в ℓ∞(ℝ), так что ghDist(X,Y) равен хаусдорфовой дистанции между образами range(Φ) и range(Ψ).
LaTeX
$$$\exists \Phi: X \to \ell_\infty(\mathbb{R}), \exists \Psi: Y \to \ell_\infty(\mathbb{R}), Isometry(\Phi) \land Isometry(\Psi) \land ghDist X Y = hausdorffDist( range(\Phi), range(\Psi) ).$$$
Lean4
/-- Two nonempty compact spaces have the same image in `GHSpace` if and only if they are
isometric. -/
theorem toGHSpace_eq_toGHSpace_iff_isometryEquiv {X : Type u} [MetricSpace X] [CompactSpace X] [Nonempty X] {Y : Type v}
[MetricSpace Y] [CompactSpace Y] [Nonempty Y] : toGHSpace X = toGHSpace Y ↔ Nonempty (X ≃ᵢ Y) :=
⟨by
simp only [toGHSpace]
rw [Quotient.eq]
rintro ⟨e⟩
have I :
(NonemptyCompacts.kuratowskiEmbedding X ≃ᵢ NonemptyCompacts.kuratowskiEmbedding Y) =
(range (kuratowskiEmbedding X) ≃ᵢ range (kuratowskiEmbedding Y)) :=
by dsimp only [NonemptyCompacts.kuratowskiEmbedding]; rfl
have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange
have g := (kuratowskiEmbedding.isometry Y).isometryEquivOnRange.symm
exact ⟨f.trans <| (cast I e).trans g⟩, by
rintro ⟨e⟩
simp only [toGHSpace]
have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange.symm
have g := (kuratowskiEmbedding.isometry Y).isometryEquivOnRange
have I :
(range (kuratowskiEmbedding X) ≃ᵢ range (kuratowskiEmbedding Y)) =
(NonemptyCompacts.kuratowskiEmbedding X ≃ᵢ NonemptyCompacts.kuratowskiEmbedding Y) :=
by dsimp only [NonemptyCompacts.kuratowskiEmbedding]; rfl
rw [Quotient.eq]
exact ⟨cast I ((f.trans e).trans g)⟩⟩
