connected_iff_exists_forall_reachable

English

A graph G is connected iff there exists a vertex v such that every vertex is reachable from v.

Русский

Граф G связан тогда и только тогда, когда существует вершина v, из которой достижимо каждое вершина.

LaTeX

$$$G.Connected \iff \exists v, \forall w, G.Reachable v w$$$

Lean4

theorem connected_iff_exists_forall_reachable : G.Connected ↔ ∃ v, ∀ w, G.Reachable v w :=
  by
  rw [connected_iff]
  constructor
  · rintro ⟨hp, ⟨v⟩⟩
    exact ⟨v, fun w => hp v w⟩
  · rintro ⟨v, h⟩
    exact ⟨fun u w => (h u).symm.trans (h w), ⟨v⟩⟩

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