toGHSpace_continuous

Mathlib.Topology.MetricSpace.GromovHausdorff

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

English

The map toGHSpace is continuous.

Русский

Отображение toGHSpace непрерывно.

LaTeX

$$Continuous(toGHSpace).$$

Lean4

theorem toGHSpace_continuous : Continuous (NonemptyCompacts.toGHSpace : NonemptyCompacts X → GHSpace) :=
  toGHSpace_lipschitz.continuous

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

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

Разделы

Аффилиация

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