mem_support_of_reachable — Mathlib

English

If there is a path from u to v with u ≠ v, then u belongs to the graph's support.

Русский

Если существует путь от u к v с u ≠ v, то u принадлежит поддержке графа.

LaTeX

$$$\forall G\, {u,v} \, (huv:\, u \neq v) \Rightarrow G.Reachable u v \Rightarrow u \in G.support$$$

Lean4

theorem mem_support_of_reachable {G : SimpleGraph V} {u v : V} (huv : u ≠ v) (h : G.Reachable u v) : u ∈ G.support :=
  by
  let p : G.Walk u v := Classical.choice h
  have hp : ¬p.Nil := Walk.not_nil_of_ne huv
  exact mem_support_of_mem_walk_support p hp p.start_mem_support

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