reachable_bot — Mathlib

English

In the empty graph (bottom), two vertices are reachable exactly when they are equal.

Русский

В пустом графе (ниже) достижимы лишь одинаковые вершины.

LaTeX

$$$(\perp : SimpleGraph\ V).Reachable u v \iff u = v.$$$

Lean4

/-- Distinct vertices are not reachable in the empty graph. -/
@[simp]
theorem reachable_bot {u v : V} : (⊥ : SimpleGraph V).Reachable u v ↔ u = v :=
  ⟨fun h ↦
    h.elim fun p ↦
      match p with
      | .nil => rfl,
    fun h ↦ h ▸ .rfl⟩

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