candidatesBDist_mem_candidatesB

Mathlib.Topology.MetricSpace.GromovHausdorffRealized

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

English

The canonical bound distance between X and Y is an element of the bound set.

Русский

Константное расстояние границы между X и Y является элементом соответствующего множества ограничений.

LaTeX

$$$candidatesBDist X Y \in candidatesB X Y$$$

Lean4

theorem candidatesBDist_mem_candidatesB : candidatesBDist X Y ∈ candidatesB X Y :=
  candidatesBOfCandidates_mem _ _

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

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

Разделы

Аффилиация

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