edist_top_of_ne

Mathlib.Combinatorics.SimpleGraph.Metric

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

English

If u ≠ v, then edist in the top graph equals 1.

Русский

Если u ≠ v, edist в верхнем графе равно 1.

LaTeX

$$$ u \neq v \Rightarrow (\top : SimpleGraph V).edist u v = 1 $$$

Lean4

theorem edist_top_of_ne (h : u ≠ v) : (⊤ : SimpleGraph V).edist u v = 1 := by simp [h]

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

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

Разделы

Аффилиация

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