Rep

Mathlib.Topology.MetricSpace.GromovHausdorff

URI: https://scilib.ai/kg/mathlib#GromovHausdorff.GHSpace.Rep

Lean4

/-- A metric space representative of any abstract point in `GHSpace` -/
def Rep (p : GHSpace) : Type :=
  (Quotient.out p : NonemptyCompacts ℓ_infty_ℝ)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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