dist_top_of_ne — Mathlib

English

In the top graph ⊤, the distance between distinct vertices is 1; if the vertices are equal, the distance is 0.

Русский

В верхнем графе ⊤ расстояние между различными вершинами равно 1; если вершины совпадают, расстояние равно 0.

LaTeX

$$$ \operatorname{dist}_{\top}(u,v) = 1 \quad\text{whenever } u \neq v.$$$

Lean4

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

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