edist_bot

Mathlib.Combinatorics.SimpleGraph.Metric

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

English

In the bottom graph, edist u v equals 0 if u = v and ⊤ otherwise.

Русский

В нижнем графе edist u v равно 0, если u = v, и ⊤ иначе.

LaTeX

$$$ (\, (\bot : SimpleGraph V).edist u v = \begin{cases}0, & u = v\\ \top, & u \neq v\end{cases} \, ) $$$

Lean4

theorem edist_bot [DecidableEq V] : (⊥ : SimpleGraph V).edist u v = (if u = v then 0 else ⊤) := by
  by_cases h : u = v <;> simp [h, edist_bot_of_ne]

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

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

Разделы

Аффилиация

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