reachable_of_mem_supp — Mathlib

English

If two vertices both lie in the same connected component’s support, then they are reachable from one another.

Русский

Если две вершины лежат в опоре одной и той же компоненты связности, то они достижимы друг из друга.

LaTeX

$$$ G.Reachable u v $ given $u, v \in C.supp$$$

Lean4

theorem reachable_of_mem_supp {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V} (hu : u ∈ C.supp)
    (hv : v ∈ C.supp) : G.Reachable u v := by
  rw [mem_supp_iff] at hu hv
  exact ConnectedComponent.exact (hv ▸ hu)

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