Chords of walks

This file defines chords and chordless walks in a simple graph.

Main definitions

• SimpleGraph.Walk.IsChord: an edge of the ambient graph between two vertices of a walk which is not an edge of the walk itself
• SimpleGraph.Walk.IsChordless: a walk with no chords

Tags

walks, chords

def SimpleGraph.Walk.IsChord {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (e : Sym2 V) : Prop

A chord of a walk p is an edge of G between two vertices of p which is not one of the edges of p.

Equations

• p.IsChord e = (e ∈ G.edgeSet ∧ e ∉ p.edges ∧ Sym2.lift ⟨fun (v_1 w : V) => v_1 ∈ p.support ∧ w ∈ p.support, ⋯⟩ e)

theorem SimpleGraph.Walk.isChord_sym2Mk {V : Type u_1} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {u' v' : V} : p.IsChord s(u', v') ↔ G.Adj u' v' ∧ s(u', v') ∉ p.edges ∧ u' ∈ p.support ∧ v' ∈ p.support

def SimpleGraph.Walk.IsChordless {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : Prop

A walk is chordless if it has no chords.

Equations

• p.IsChordless = ∀ ⦃e : Sym2 V⦄, ¬p.IsChord e

theorem SimpleGraph.Walk.isChordless_iff_forall_mem_edges {V : Type u_1} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.IsChordless ↔ ∀ ⦃u' v' : V⦄, u' ∈ p.support → v' ∈ p.support → G.Adj u' v' → s(u', v') ∈ p.edges

theorem SimpleGraph.Walk.IsChordless.mem_edges {V : Type u_1} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.IsChordless) {u' v' : V} (hu' : u' ∈ p.support) (hv' : v' ∈ p.support) (hadj : G.Adj u' v') : s(u', v') ∈ p.edges