reachable_iff_nonempty_univ — Mathlib

English

For any graph G and vertices u,v, u is reachable from v iff there exists a walk from u to v.

Русский

Для любого графа G и вершин u, v верно: u достижим из v тогда и только тогда, когда существует путь (ход) от u к v.

LaTeX

$$$G.Reachable(u,v) \iff \exists p: G.Walk\,u\,v.$$$

Lean4

theorem reachable_iff_nonempty_univ {u v : V} : G.Reachable u v ↔ (Set.univ : Set (G.Walk u v)).Nonempty :=
  Set.nonempty_iff_univ_nonempty

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