rep_gHSpace_compactSpace

Mathlib.Topology.MetricSpace.GromovHausdorff

URI: https://scilib.ai/kg/mathlib#GromovHausdorff.rep_gHSpace_compactSpace

English

For any p in GHSpace, p.Rep is nonempty.

Русский

Для любого p из GHSpace, p.Rep непусто.

LaTeX

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

Lean4

instance rep_gHSpace_compactSpace {p : GHSpace} : CompactSpace p.Rep :=
  inferInstanceAs <| CompactSpace p.out

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru