repGHSpaceMetricSpace — Mathlib

English

For any p in the Gromov–Hausdorff space, the underlying representative p.Rep is a compact space.

Русский

Для каждого p в пространстве Громова–Хаусдорфа, соответствующий представитель p.Rep является компактным пространством.

LaTeX

$$For any p : GHSpace, CompactSpace p.Rep.$$

Lean4

instance repGHSpaceMetricSpace {p : GHSpace} : MetricSpace p.Rep :=
  inferInstanceAs <| MetricSpace p.out

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