dist_nndist

Mathlib.Topology.MetricSpace.Pseudo.Defs

URI: https://scilib.ai/kg/mathlib#dist_nndist

English

In a pseudometric space, dist x y = nndist x y.

Русский

В псевдометрическом пространстве расстояние между x и y равно nndist x y.

LaTeX

$$dist x y = nndist x y$$

Lean4

/-- Express `dist` in terms of `nndist` -/
theorem dist_nndist (x y : α) : dist x y = nndist x y :=
  rfl

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

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

Разделы

Аффилиация

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