Native induced embeddings of chordless cycles

The vertices of a chordless cycle, indexed before the repeated endpoint, give an induced embedding of Mathlib's cycle graph. A cycle of length at least six then contains an induced pair of disjoint edges.

theorem SimpleGraph.Walk.IsCycle.adj_getVert_iff_of_isChordless {V : Type u_1} {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hc : p.IsCycle) (hh : p.IsChordless) {i j : ℕ} (hi : i < p.length) (hj : j < p.length) : G.Adj (p.getVert i) (p.getVert j) ↔ i + 1 = j ∨ j + 1 = i ∨ i = 0 ∧ j + 1 = p.length ∨ j = 0 ∧ i + 1 = p.length

Adjacency along a chordless cycle is precisely consecutive or wraparound adjacency.

theorem SimpleGraph.Walk.IsCycle.cycleGraph_isIndContained_of_isChordless {V : Type u_1} {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hc : p.IsCycle) (hh : p.IsChordless) : (cycleGraph p.length).IsIndContained G

A chordless cycle supplies a native induced embedding of the cycle graph.

theorem SimpleGraph.Walk.IsCycle.twoK2_isIndContained_of_isChordless {V : Type u_1} {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hc : p.IsCycle) (hh : p.IsChordless) (hlen : 6 ≤ p.length) : (⊤ ⊕g ⊤).IsIndContained G

A chordless cycle of length at least six has an induced disjoint pair of edges.