dist_bot — Mathlib

English

Let G be a SimpleGraph on V and consider the bottom graph ⊥. Then the distance between any two vertices u and v in ⊥ is 0.

Русский

Пусть G — простой граф на V и рассмотрим нижний граф ⊥. Тогда расстояние между любыми вершинами u и v в ⊥ равно 0.

LaTeX

$$$ \operatorname{dist}_{\perp}(u,v) = 0 $$$

Lean4

@[simp]
theorem dist_bot : (⊥ : SimpleGraph V).dist u v = 0 := by by_cases h : u = v <;> simp [h]

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