dist_comm

Mathlib.Topology.MetricSpace.PiNat

URI: https://scilib.ai/kg/mathlib#PiNat.dist_comm

English

Distance is symmetric: dist(x,y) = dist(y,x).

Русский

Расстояние симметрично: dist(x,y) = dist(y,x).

LaTeX

$$$$ \operatorname{dist}(x,y)=\operatorname{dist}(y,x) $$$$

Lean4

protected theorem dist_comm (x y : ∀ n, E n) : dist x y = dist y x := by
  classical simp [dist, @eq_comm _ x y, firstDiff_comm]

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

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

Разделы

Аффилиация

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