dist_comm

Mathlib.Combinatorics.SimpleGraph.Metric

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

English

Distance is symmetric: dist_G(u,v) = dist_G(v,u).

Русский

Расстояние симметрично: dist_G(u,v) = dist_G(v,u).

LaTeX

$$$$ \mathrm{dist}_G(u,v) = \mathrm{dist}_G(v,u) $$$$

Lean4

theorem dist_comm : G.dist u v = G.dist v u := by rw [dist, dist, edist_comm]

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

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

Разделы

Аффилиация

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