instDistGHSpace — Mathlib

English

For any p, q in GHSpace, the distance dist p q equals ghDist p.Rep q.Rep.

Русский

Для любых p, q в GHSpace расстояние dist p q равно ghDist p.Rep q.Rep.

LaTeX

$$For p, q : GHSpace, dist p q = ghDist p.Rep q.Rep.$$

Lean4

/-- Distance on `GHSpace`: the distance between two nonempty compact spaces is the infimum
Hausdorff distance between isometric copies of the two spaces in a metric space. For the definition,
we only consider embeddings in `ℓ^∞(ℝ)`, but we will prove below that it works for all spaces. -/
instance : Dist GHSpace where
  dist x
    y :=
    sInf <|
      (fun p : NonemptyCompacts ℓ_infty_ℝ × NonemptyCompacts ℓ_infty_ℝ => hausdorffDist (p.1 : Set ℓ_infty_ℝ) p.2) ''
        {a | ⟦a⟧ = x} ×ˢ {b | ⟦b⟧ = y}

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