reachable_iff_exists_finsetWalkLength_nonempty

English

For any u, v, in a finite vertex graph, G.Reachable u v holds iff there exists a finite n such that there is a path from u to v of length n.

Русский

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

LaTeX

$$$G.Reachable(u,v) \iff \exists n < |V| \text{ such that } (G.finsetWalkLength\, n\, u \, v).Nonempty$$$

Lean4

theorem reachable_iff_exists_finsetWalkLength_nonempty (u v : V) :
    G.Reachable u v ↔ ∃ n : Fin (Fintype.card V), (G.finsetWalkLength n u v).Nonempty :=
  by
  constructor
  · intro r
    refine r.elim_path fun p => ?_
    refine ⟨⟨_, p.isPath.length_lt⟩, p, ?_⟩
    simp [mem_finsetWalkLength_iff]
  · rintro ⟨_, p, _⟩
    exact ⟨p⟩

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