candidatesBOfCandidates

Mathlib.Topology.MetricSpace.GromovHausdorffRealized

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

← MathLib Explorer

English

GHSpace is a complete metric space.

Русский

GHSpace — полное метрическое пространство.

LaTeX

$$Instance: CompleteSpace GHSpace.$$

Lean4

/-- candidates give rise to elements of `BoundedContinuousFunction`s -/
def candidatesBOfCandidates (f : ProdSpaceFun X Y) (fA : f ∈ candidates X Y) : Cb X Y :=
  BoundedContinuousFunction.mkOfCompact ⟨f, (candidates_lipschitz fA).continuous⟩

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

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

Разделы

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

Аффилиация

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