edist_top — Mathlib

English

For all u,v, the extended distance in the top graph is 0 if u=v and 1 otherwise.

Русский

Для любых вершин u,v - расстояние в верхнем графе равно 0, если u=v, и 1 в противном случае.

LaTeX

$$$ \forall u,v, G.edist u v = (\text{if } u=v \text{ then } 0 \text{ else } 1) $$$

Lean4

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

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