Theorems · Theorem · combinatorics

SimpleGraph.Walk.IsTrail.isEdgeReachable_two_of_isEdgeReachable_two

∀ {V : Type u_1} {G : SimpleGraph V} {u v x y : V} {w : G.Walk u v},
  w.IsTrail → G.IsEdgeReachable 2 u v → x ∈ w.support → y ∈ w.support → G.IsEdgeReachable 2 x y

Vertices of a trail with 2-edge reachable endpoints are 2-edge reachable.

Defined in

Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Cited by

1 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound