ghDist_le_nonemptyCompacts_dist — Mathlib

English

GHSpace carries a natural topology coming from its metric structure (and is compatible with the underlying uniform structure).

Русский

GHSpace имеет естественную топологию, порожденную его метрическим структуром и совместимую с униформной структурой.

LaTeX

$$GHSpace : TopologicalSpace$$

Lean4

theorem ghDist_le_nonemptyCompacts_dist (p q : NonemptyCompacts X) : dist p.toGHSpace q.toGHSpace ≤ dist p q :=
  by
  have ha : Isometry ((↑) : p → X) := isometry_subtype_coe
  have hb : Isometry ((↑) : q → X) := isometry_subtype_coe
  have A : dist p q = hausdorffDist (p : Set X) q := rfl
  have I : ↑p = range ((↑) : p → X) := Subtype.range_coe_subtype.symm
  have J : ↑q = range ((↑) : q → X) := Subtype.range_coe_subtype.symm
  rw [A, I, J]
  exact ghDist_le_hausdorffDist ha hb

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