def SimpleGraph.InternallyDisjoint {V : Type u_2} {G : SimpleGraph V} {u v x y : V} (p : G.Walk u v) (q : G.Walk x y) : Prop

Two walks are internally disjoint if they share no vertices other than their endpoints.

Equations

• SimpleGraph.InternallyDisjoint p q = p.support.tail.dropLast.Disjoint q.support.tail.dropLast

def SimpleGraph.InfinitelyConnected {V : Type u_2} (G : SimpleGraph V) : Prop

We say a graph is infinitely connected if any two vertices are connected by infinitely many pairwise disjoint paths. Note that graphs with at most one vertex are not classed as infinitely connected.

Equations

• G.InfinitelyConnected = (Nontrivial V ∧ Pairwise fun (u v : V) => ∃ (P : Set (G.Walk u v)), P.Infinite ∧ (∀ p ∈ P, p.IsPath) ∧ P.Pairwise SimpleGraph.InternallyDisjoint)