def WList.lineGraphEdgeWalk {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) : WList β (Sym2 β)

Walk on L(G) whose vertices are the edges of a nonempty walk in G.

Equations

• WList.lineGraphEdgeWalk hw_2 = WList.nil e
• WList.lineGraphEdgeWalk hw_2 = WList.cons e s(e, f) (WList.lineGraphEdgeWalk ⋯)

@[simp]

theorem WList.lineGraphEdgeWalk_firstEdge {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) : (lineGraphEdgeWalk hw).first = Nonempty.firstEdge w hw

theorem WList.lineGraphEdgeWalk_lastEdge {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) : (lineGraphEdgeWalk hw).last = Nonempty.lastEdge w hw

theorem Graph.lineGraph_deleteVerts_deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} (F : Set β) : (G.deleteEdges F).LineGraph = G.LineGraph.deleteVerts F

instance Graph.instFiniteSym2LineGraph {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] : G.LineGraph.Finite

theorem Graph.connBetween_restrict_of_inc_same_edge {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} (hu : G.Inc e u) (hv : G.Inc e v) : (G.restrict {e}).ConnBetween u v

theorem Graph.lineGraph_isWalk_restrict_connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {W : WList β (Sym2 β)} (hW : G.LineGraph.IsWalk W) ⦃u v : α⦄ : W.first ∈ E(G, u) → W.last ∈ E(G, v) → (G.restrict W.vertexSet).ConnBetween u v

theorem Graph.IsPath.lineGraphEdgeWalk_isWalk {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} (hw : w.Nonempty) (hP : G.IsPath w) : G.LineGraph.IsWalk (WList.lineGraphEdgeWalk hw)

theorem Graph.connBetween_of_mem_incEdges_same_edge {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} (hu : G.Inc e u) (hv : G.Inc e v) : G.ConnBetween u v

theorem Graph.lineGraph_isWalk_connBetween_of_mem_inc {α : Type u_1} {β : Type u_2} {G : Graph α β} {W : WList β (Sym2 β)} (hW : G.LineGraph.IsWalk W) {u v : α} : W.first ∈ E(G, u) → W.last ∈ E(G, v) → G.ConnBetween u v

theorem Graph.IsPath.inc_firstEdge_inc {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) (hne : P.first ≠ P.last) : G.Inc (WList.Nonempty.firstEdge P ⋯) P.first

theorem Graph.IsPath.inc_lastEdge_inc {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) (hne : P.first ≠ P.last) : G.Inc (WList.Nonempty.lastEdge P ⋯) P.last

theorem Graph.lineGraph_setConnected_incEdges_iff {α : Type u_1} {β : Type u_2} {s t : α} (G : Graph α β) (hst : s ≠ t) : G.LineGraph.SetConnected E(G, s) E(G, t) ↔ G.ConnBetween s t

theorem Graph.lineGraph_deleteVerts_setConnected_incEdges_iff' {α : Type u_1} {β : Type u_2} {s t : α} (G : Graph α β) (hst : s ≠ t) (F : Set β) : (G.LineGraph.deleteVerts F).SetConnected E(G.deleteEdges F, s) E(G.deleteEdges F, t) ↔ (G.deleteEdges F).ConnBetween s t

theorem Graph.lineGraph_deleteVerts_setConnected_incEdges_iff {α : Type u_1} {β : Type u_2} {s t : α} (G : Graph α β) (hst : s ≠ t) (F : Set β) : (G.LineGraph.deleteVerts F).SetConnected E(G, s) E(G, t) ↔ (G.deleteEdges F).ConnBetween s t

@[simp]

theorem Graph.isEdgeCutBetween_iff_lineGraph_isSetCut {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} (hst : s ≠ t) (F : Set β) : G.IsEdgeCutBetween F s t ↔ G.LineGraph.IsSetCut E(G, s) E(G, t) F

@[simp]

theorem Graph.edgeConnBetweenGE_iff_lineGraph_setConnGE {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} (hst : s ≠ t) (n : ℕ) : G.EdgeConnBetweenGE s t n ↔ G.LineGraph.SetConnGE E(G, s) E(G, t) n