theorem Graph.IsWalk.edgeRemove_contract_nil {α : Type u_1} {β : Type u_2} {G : Graph α β} [DecidablePred fun (x : β) => x ∈ G.edgeSet] {w : WList α β} (φ : α → α) (hw : G.IsWalk w) : (WList.edgeRemove G.edgeSet (WList.map φ w)).Nil

theorem Graph.IsWalk.mem_map_iff_first_of_isRepFun {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {φ : α → α} [DecidablePred fun (x : β) => x ∈ G.edgeSet] (hφ : G.connPartition.IsRepFun φ) {w : WList α β} (hw : G.IsWalk w) : x ∈ WList.map φ w ↔ x = φ w.first

theorem Graph.IsWalk.mem_map_iff_last_of_isRepFun {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {φ : α → α} [DecidablePred fun (x : β) => x ∈ G.edgeSet] (hφ : G.connPartition.IsRepFun φ) {w : WList α β} (hw : G.IsWalk w) : x ∈ WList.map φ w ↔ x = φ w.last

noncomputable def Graph.IsWalk.uncontract_aux {α : Type u_1} {β : Type u_2} {G H : Graph α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) {u v : α} {W : WList α β} (hw : H /[G.edgeSet, φ].IsWalk W) (hu : W.first = φ u) (hv : W.last = φ v) : { w : WList α β // w.first = u ∧ w.last = v }

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Graph.IsWalk.uncontract {α : Type u_1} {β : Type u_2} {u v : α} {G H : Graph α β} {W : WList α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) (hw : H /[G.edgeSet, φ].IsWalk W) (hu : W.first = φ u) (hv : W.last = φ v) : WList α β

Equations

• Graph.IsWalk.uncontract hφ hw hu hv = ↑(Graph.IsWalk.uncontract_aux hφ hw hu hv)

@[simp]

theorem Graph.IsWalk.uncontract_first {α : Type u_1} {β : Type u_2} {u v : α} {G H : Graph α β} {W : WList α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) (hw : H /[G.edgeSet, φ].IsWalk W) (hu : W.first = φ u) (hv : W.last = φ v) : (uncontract hφ hw hu hv).first = u

@[simp]

theorem Graph.IsWalk.uncontract_last {α : Type u_1} {β : Type u_2} {u v : α} {G H : Graph α β} {W : WList α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) (hw : H /[G.edgeSet, φ].IsWalk W) (hu : W.first = φ u) (hv : W.last = φ v) : (uncontract hφ hw hu hv).last = v

theorem Graph.IsWalk.uncontract_map_edgeRemove {α : Type u_1} {β : Type u_2} {u v : α} {G H : Graph α β} {W : WList α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) [DecidablePred fun (x : β) => x ∈ G.edgeSet] (hw : H /[G.edgeSet, φ].IsWalk W) (hu : W.first = φ u) (hv : W.last = φ v) : WList.edgeRemove G.edgeSet (WList.map φ (uncontract hφ hw hu hv)) = W

@[simp]

theorem Graph.IsWalk.unedgeSet_contract_diff {α : Type u_1} {β : Type u_2} {u v : α} {G H : Graph α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) {W : WList α β} (hw : H /[G.edgeSet, φ].IsWalk W) (hu : W.first = φ u) (hv : W.last = φ v) : (uncontract hφ hw hu hv).edgeSet \ G.edgeSet = W.edgeSet

@[simp]

theorem Graph.IsWalk.subset_unedgeSet_contract {α : Type u_1} {β : Type u_2} {u v : α} {G H : Graph α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) {W : WList α β} (hw : H /[G.edgeSet, φ].IsWalk W) (hu : W.first = φ u) (hv : W.last = φ v) : W.edgeSet ⊆ (uncontract hφ hw hu hv).edgeSet

@[simp]

theorem Graph.IsWalk.unedgeSet_contract_subset {α : Type u_1} {β : Type u_2} {u v : α} {G H : Graph α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) {W : WList α β} (hw : H /[G.edgeSet, φ].IsWalk W) (hu : W.first = φ u) (hv : W.last = φ v) : (uncontract hφ hw hu hv).edgeSet ⊆ W.edgeSet ∪ G.edgeSet

theorem Graph.IsWalk.uncontract_isWalk {α : Type u_1} {β : Type u_2} {u v : α} {G H : Graph α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) (hGH : G ≤ H) {W : WList α β} (hw : H /[G.edgeSet, φ].IsWalk W) (hu : W.first = φ u) (hv : W.last = φ v) : H.IsWalk (uncontract hφ hw hu hv)

@[simp]

theorem Graph.IsWalk.mem_uncontract_map_iff {α : Type u_1} {β : Type u_2} {x u v : α} {G H : Graph α β} {W : WList α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) (hGH : G ≤ H) (hw : H /[G.edgeSet, φ].IsWalk W) (hu : W.first = φ u) (hv : W.last = φ v) : x ∈ WList.map φ (uncontract hφ hw hu hv) ↔ x ∈ W

theorem Graph.IsPath.uncontract_isPath {α : Type u_1} {β : Type u_2} {u v : α} {G H : Graph α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) (hGH : G ≤ H) {W : WList α β} (hw : H /[G.edgeSet, φ].IsPath W) (hu : W.first = φ u) (hv : W.last = φ v) : H.IsPath (IsWalk.uncontract hφ ⋯ hu hv)

theorem Graph.IsCyclicWalk.exists_isCyclicWalk_of_contract {α : Type u_1} {β : Type u_2} {G H : Graph α β} {W : WList α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) (hGH : G ≤ H) (hw : H /[G.edgeSet, φ].IsCyclicWalk W) : ∃ (C : WList α β), H.IsCyclicWalk C ∧ C.edgeSet \ G.edgeSet = W.edgeSet

theorem Graph.contract_connBetween_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) (hGH : G ≤ H) (u v : α) : H /[G.edgeSet, φ].ConnBetween (φ u) (φ v) ↔ H.ConnBetween u v

@[simp]

theorem Graph.contract_preconnected_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) (hGH : G ≤ H) : H /[G.edgeSet, φ].Preconnected ↔ H.Preconnected

@[simp]

theorem Graph.contract_connected_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) (hGH : G ≤ H) : H /[G.edgeSet, φ].Connected ↔ H.Connected

theorem Graph.contract_isBridge_iff {α : Type u_1} {β : Type u_2} {e : β} {G H : Graph α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) (hGH : G ≤ H) (he : e ∈ H.edgeSet \ G.edgeSet) : H /[G.edgeSet, φ].IsBridge e ↔ H.IsBridge e

theorem Graph.IsForest.contract {α : Type u_1} {β : Type u_2} {G H : Graph α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) (hGH : G ≤ H) (hH : H.IsForest) : H /[G.edgeSet, φ].IsForest

def Graph.minorMap.trans {α : Type u_1} {β : Type u_2} {G H I : Graph α β} (F₁ : G.minorMap H) (F₂ : H.minorMap I) : G.minorMap I

Equations

• F₁.trans F₂ = { map := fun (v : ↑G.vertexSet) => (F₂.anti_left ⋯).intermediate, map_le := ⋯, mem_map := ⋯, disj := ⋯, edge_disj := ⋯, link := ⋯, conn := ⋯ }

theorem Graph.IsMinor.trans {α : Type u_1} {β : Type u_2} {G H I : Graph α β} (hGH : G ≤m H) (hHI : H ≤m I) : G ≤m I

instance Graph.instIsPreorderIsMinor {α : Type u_1} {β : Type u_2} : IsPreorder (Graph α β) IsMinor