edist_ofDual

Mathlib.Topology.EMetricSpace.Defs

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

English

For duals, the extended distance is preserved: edist(ofDual a, ofDual b) = edist a b.

Русский

Для двойственных объектов сохраняется расширенное расстояние: edist(ofDual a, ofDual b) = edist a b.

LaTeX

$$$\\mathrm{edist}(\\mathrm{ofDual}\\ a, \\mathrm{ofDual}\\ b) = \\mathrm{edist}(a,b)$$$

Lean4

@[simp]
theorem edist_ofDual (a b : Xᵒᵈ) : edist (ofDual a) (ofDual b) = edist a b :=
  rfl

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

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

Разделы

Аффилиация

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