dist_toDual

Mathlib.Topology.MetricSpace.Defs

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

English

Distance is preserved under the dualization map: dist(toDual a, toDual b) = dist a b.

Русский

Расстояние сохраняется при переходе к двойственному представлению: dist(toDual a, toDual b) = dist a b.

LaTeX

$$dist\; (toDual\; a)\; (toDual\; b) = dist\; a\; b$$

Lean4

@[simp]
theorem dist_toDual (a b : X) : dist (toDual a) (toDual b) = dist a b :=
  rfl

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

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

Разделы

Аффилиация

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