English
Let X be a nonempty compact metric space and p a nonempty compact subset of the Kuratowski embedding target. Then the class ⟦p⟧ in the Gromov–Hausdorff space of X equals the realization toGHSpace(X) if and only if there exists an isometry Ψ: X → ℓ∞(ℝ) with image equal to p.
Русский
Пусть X – непустое компактное метрическое множество и p – непустое компактное множество в целевой площади Куротовского вложения. Тогда элемент ⟦p⟧ в пространстве Громова–Хаусдорфа равен образу X в toGHSpace(X) тогда и только тогда, когда существует изометрия Ψ: X → ℓ∞(ℝ) с образцом p.
LaTeX
$$$\langle p\rangle = toGHSpace(X) \iff \exists \Psi: X \to \ell_\infty(\mathbb{R}),\ Isometry\ \Psi \land range(\Psi) = p.$$$
Lean4
theorem eq_toGHSpace_iff {X : Type u} [MetricSpace X] [CompactSpace X] [Nonempty X] {p : NonemptyCompacts ℓ_infty_ℝ} :
⟦p⟧ = toGHSpace X ↔ ∃ Ψ : X → ℓ_infty_ℝ, Isometry Ψ ∧ range Ψ = p :=
by
simp only [toGHSpace, Quotient.eq]
refine ⟨fun h => ?_, ?_⟩
· rcases Setoid.symm h with ⟨e⟩
have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange.trans e
use fun x => f x, isometry_subtype_coe.comp f.isometry
rw [range_comp', f.range_eq_univ, Set.image_univ, Subtype.range_coe]
· rintro ⟨Ψ, ⟨isomΨ, rangeΨ⟩⟩
have f := ((kuratowskiEmbedding.isometry X).isometryEquivOnRange.symm.trans isomΨ.isometryEquivOnRange).symm
have E : (range Ψ ≃ᵢ NonemptyCompacts.kuratowskiEmbedding X) = (p ≃ᵢ range (kuratowskiEmbedding X)) := by
dsimp only [NonemptyCompacts.kuratowskiEmbedding]; rw [rangeΨ]; rfl
exact ⟨cast E f⟩
