theorem Graph.ConnBetween.eq_or_isLink_of_edgeSet_singleton {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.ConnBetween x y) (hE : G.edgeSet = {e}) : x = y ∨ G.IsLink e x y

@[simp]

theorem Graph.connBetween_isRepFun_left_iff {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) : G.ConnBetween (φ x) y ↔ G.ConnBetween x y

@[simp]

theorem Graph.connBetween_isRepFun_right_iff {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) : G.ConnBetween x (φ y) ↔ G.ConnBetween x y

Contracting a set of edges

def Graph.contract {α : Type u_1} {β : Type u_2} {α' : Type u_5} (G : Graph α β) (C : Set β) (φ : α → α') : Graph α' β

Contract G C φ contracts the edges in set C of graph G, mapping the resulting vertices according to function φ.

This operation creates a new graph where:

1. Edges in set C are removed
2. Vertices are relabeled according to the mapping function φ

This definition does not enforce that φ should relate to C in any way. For this definition to be sound, φ has to have the connected components of G ↾ C as fibers.

Equations

• G /[C, φ] = (Graph.map φ G).deleteEdges C

@[simp]

theorem Graph.edgeSet_contract {α : Type u_1} {β : Type u_2} {α' : Type u_5} (G : Graph α β) (C : Set β) (φ : α → α') : G /[C, φ].edgeSet = G.edgeSet \ C

@[simp]

theorem Graph.contract_isLink {α : Type u_1} {β : Type u_2} {α' : Type u_5} (G : Graph α β) (C : Set β) (φ : α → α') (e : β) (x y : α') : G /[C, φ].IsLink e x y = ((∃ (x_1 : α) (y_1 : α), G.IsLink e x_1 y_1 ∧ x = φ x_1 ∧ y = φ y_1) ∧ e ∉ C)

@[simp]

theorem Graph.vertexSet_contract {α : Type u_1} {β : Type u_2} {α' : Type u_5} (G : Graph α β) (C : Set β) (φ : α → α') : G /[C, φ].vertexSet = φ '' G.vertexSet

def Graph.«term_/[_,_]» : Lean.TrailingParserDescr

Equations

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

@[simp]

theorem Graph.contract_inc {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {α' : Type u_5} {φ : α → α'} {C : Set β} {x : α'} : G /[C, φ].Inc e x ↔ e ∉ C ∧ ∃ (v : α), G.Inc e v ∧ φ v = x

theorem Graph.IsLink.contract_of_notMem {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} {α' : Type u_5} {C : Set β} (φ : α → α') (heC : e ∉ C) (hbtw : G.IsLink e u v) : G /[C, φ].IsLink e (φ u) (φ v)

theorem Graph.IsLoopAt.contract_of_notMem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {α' : Type u_5} {C : Set β} (φ : α → α') (heC : e ∉ C) (hbtw : G.IsLoopAt e x) : G /[C, φ].IsLoopAt e (φ x)

theorem Graph.contract_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} {α' : Type u_5} {φ : α → α'} {C : Set β} (h : G ≤ H) : G /[C, φ] ≤ H /[C, φ]

theorem Graph.contract_isSpanningSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {α' : Type u_5} {φ : α → α'} {C : Set β} (h : G ≤s H) : G /[C, φ] ≤s H /[C, φ]

@[simp]

theorem Graph.contract_contract {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_5} {α'' : Type u_6} {φ : α → α'} {C C' : Set β} {φ' : α' → α''} : G /[C, φ] /[C', φ'] = G /[C ∪ C', φ' ∘ φ]

theorem Graph.contract_restrict_comm {α : Type u_1} {β : Type u_2} {H : Graph α β} {F : Set β} {α' : Type u_5} {φ : α → α'} {C : Set β} : H /[C, φ].restrict F = H.restrict F /[C, φ]

theorem Graph.contract_deleteEdges_comm {α : Type u_1} {β : Type u_2} {H : Graph α β} {F : Set β} {α' : Type u_5} {φ : α → α'} {C : Set β} : H /[C, φ].deleteEdges F = H.deleteEdges F /[C, φ]

theorem Graph.edgeSet_disjoint_of_le_contract {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : Set β} {φ : α → α} (h : G ≤ G /[C, φ]) : Disjoint G.edgeSet C

theorem Graph.edgeSet_disjoint_of_le_contract_ge {α : Type u_1} {β : Type u_2} {G H I : Graph α β} {φ : α → α} (h : G ≤ H /[I.edgeSet, φ]) : Disjoint G.edgeSet I.edgeSet

@[simp]

theorem Graph.contract_eq_map_of_disjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_5} {φ : α → α'} {C : Set β} (hdj : Disjoint G.edgeSet C) : G /[C, φ] = map φ G

theorem Graph.map_eq_self_of_contract_eq_self {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : Set β} {φ : α → α} (h : G /[C, φ] = G) : map φ G = G

theorem Partition.IsRepFun.isContractClosed {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : Set β} {φ : α → α} (hφ : (G.restrict C).connPartition.IsRepFun φ) : G.IsContractClosed φ C

theorem Partition.IsRepFun.isContractClosed_of_compatible {α : Type u_1} {β : Type u_2} {G H : Graph α β} {φ : α → α} (hφ : H.connPartition.IsRepFun φ) (hGH : G.Compatible H) : G.IsContractClosed φ H.edgeSet

theorem Partition.IsRepFun.isContractClosed_of_ge {α : Type u_1} {β : Type u_2} {G H : Graph α β} {φ : α → α} (hφ : H.connPartition.IsRepFun φ) (hHG : H ≤ G) : G.IsContractClosed φ H.edgeSet

@[simp]

theorem Graph.preimage_deleteVerts_contract {α : Type u_1} {β : Type u_2} {H : Graph α β} {X : Set α} {C : Set β} {φ : α → α} : H.deleteVerts (φ ⁻¹' X) /[C, φ] = H /[C, φ].deleteVerts X

@[simp]

theorem Graph.preimage_induce_contract {α : Type u_1} {β : Type u_2} {H : Graph α β} {X : Set α} {C : Set β} {φ : α → α} (hX : X ⊆ φ '' H.vertexSet) : H[φ ⁻¹' X] /[C, φ] = (H /[C, φ])[X]

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

theorem Graph.le_contract_comm {α : Type u_1} {β : Type u_2} {G H I : Graph α β} {φ : α → α} (_hφ : I.connPartition.IsRepFun φ) (_hI : I ≤ H) : G ≤ H /[I.edgeSet, φ] ↔ ∃ H' ≤ H, G = H' /[I.edgeSet, φ]

theorem Graph.isLoopAt_map_iff_connBetween {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} {φ : α → α} (hφ : G.connPartition.IsRepFun φ) : (map φ H).IsLoopAt e x ↔ ∃ (u : α) (v : α), H.IsLink e u v ∧ (u = v ∨ G.ConnBetween u v) ∧ φ u = x

theorem Graph.IsWalk.edgeRemove_contract {α : Type u_1} {β : Type u_2} {G H : Graph α β} {φ : α → α} [DecidablePred fun (x : β) => x ∈ H.edgeSet] {w : WList α β} (h : G.IsWalk w) (hHG : H ≤ G) (hφ : H.connPartition.IsRepFun φ) : G /[H.edgeSet, φ].IsWalk (WList.edgeRemove H.edgeSet (WList.map φ w))

theorem Graph.IsTrail.edgeRemove_contract {α : Type u_1} {β : Type u_2} {G H : Graph α β} {φ : α → α} [DecidablePred fun (x : β) => x ∈ H.edgeSet] {w : WList α β} (h : G.IsTrail w) (hHG : H ≤ G) (hφ : H.connPartition.IsRepFun φ) : G /[H.edgeSet, φ].IsTrail (WList.edgeRemove H.edgeSet (WList.map φ w))

theorem Graph.IsTour.edgeRemove_contract {α : Type u_1} {β : Type u_2} {G H : Graph α β} {φ : α → α} [DecidablePred fun (x : β) => x ∈ H.edgeSet] {w : WList α β} (h : G.IsTour w) (hHG : H ≤ G) (hφ : H.connPartition.IsRepFun φ) (hne : ∃ e ∈ w.edge, e ∉ H.edgeSet) : G /[H.edgeSet, φ].IsTour (WList.edgeRemove H.edgeSet (WList.map φ w))

Contraction of one edge

def Graph.IsLink.repFun {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} [DecidableEq α] : G.IsLink e x y → α → α

A representative function for the connected components of G ↾ {e} coming from a link G.IsLink e x y: it identifies y with x and fixes all other vertices.

Equations

• x✝.repFun v = if v = y then x else v

theorem Graph.IsLink.isRepFun {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} [DecidableEq α] (he : G.IsLink e x y) : (G.restrict {e}).connPartition.IsRepFun he.repFun

@[simp]

theorem Graph.IsLink.repFun_apply {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} [DecidableEq α] (he : G.IsLink e x y) (v : α) : he.repFun v = if v = y then x else v

@[simp]

theorem Graph.IsLink.repFun_apply_of_ne {α : Type u_1} {β : Type u_2} {x y v : α} {e : β} {G : Graph α β} [DecidableEq α] (he : G.IsLink e x y) (hne : v ≠ y) : he.repFun v = v

@[simp]

theorem Graph.IsLink.repFun_apply_right {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} [DecidableEq α] (he : G.IsLink e x y) : he.repFun y = x

theorem Graph.IsLink.repFun_toFun {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} [DecidableEq α] (he : G.IsLink e x y) : he.repFun = fun (v : α) => if v = y then x else v

@[simp]

theorem Graph.IsLink.repFun_preimage {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} [DecidableEq α] (he : G.IsLink e x y) (S : Set α) [DecidablePred fun (x : α) => x ∈ S] : he.repFun ⁻¹' S = if x ∈ S then insert y S else S \ {y}

def Graph.IsLink.contract {α : Type u_1} {β : Type u_2} {x y : α} (G : Graph α β) (e : β) (he : G.IsLink e x y) : Graph α β

Contracts the edge given in the IsLink predicate by removing the second vertex and adding its edges to the first vertex.

Equations

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

@[simp]

theorem Graph.IsLink.vertexSet_contract {α : Type u_1} {β : Type u_2} {x y : α} (G : Graph α β) (e : β) (he : G.IsLink e x y) : G /(e, he).vertexSet = insert x (G.vertexSet \ {y})

@[simp]

theorem Graph.IsLink.edgeSet_contract {α : Type u_1} {β : Type u_2} {x y : α} (G : Graph α β) (e : β) (he : G.IsLink e x y) : G /(e, he).edgeSet = G.edgeSet \ {e}

@[simp]

theorem Graph.IsLink.contract_isLink {α : Type u_1} {β : Type u_2} {x y : α} (G : Graph α β) (e : β) (he : G.IsLink e x y) (f : β) (u v : α) : G /(e, he).IsLink f u v = ∃ (a : α) (b : α), (G.IsLink f a b ∧ f ≠ e) ∧ (a = y ∧ x = u ∨ a ≠ y ∧ a = u) ∧ (b = y ∧ x = v ∨ b ≠ y ∧ b = v)

def Graph.IsLink.«term_/(_,_)» : Lean.TrailingParserDescr

Equations

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

theorem Graph.IsLink.vertexSet_contract_of_ne {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (he : G.IsLink e x y) (hxy : x ≠ y) : G /(e, he).vertexSet = G.vertexSet \ {y}

theorem Graph.IsLink.contract_vertex_encard_eq_add_one {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} [G.Finite] (he : G.IsLink e x y) (hxy : x ≠ y) : G.vertexSet.encard = G /(e, he).vertexSet.encard + 1

Equality to a map/delete presentation

theorem Graph.IsLink.contract_deleteVerts_of_notMem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {X : Set α} (he : G.IsLink e x y) (hx : x ∉ X) : G /(e, he).deleteVerts X = G.deleteVerts (X \ {y}) /(e, ⋯)

theorem Graph.IsLink.contract_eq_map_deleteEdges {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} [DecidableEq α] (he : G.IsLink e x y) : G /(e, he) = Graph.map he.repFun (G.deleteEdges {e})

@[simp]

theorem Graph.IsLoopAt.contract_eq {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} [DecidableEq α] (he : G.IsLoopAt e x) : G /(e, ⋯) = G.deleteEdges {e}

theorem Graph.IsLink.contract_eq {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} [DecidableEq α] (he : G.IsLink e x y) : G /(e, he) = G /[{e}, he.repFun]

theorem Graph.IsLink.contract_isLink_of_ne {α : Type u_1} {β : Type u_2} {x y u v : α} {e f : β} {G : Graph α β} [DecidableEq α] (he : G.IsLink e x y) (hf : G.IsLink f u v) (hef : e ≠ f) : G /(e, he).IsLink f (he.repFun u) (he.repFun v)

theorem Graph.IsLink.contract_deleteEdges_comm {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {F : Set β} [DecidableEq α] (he : G.IsLink e x y) (heF : e ∉ F) : G /(e, he).deleteEdges F = G.deleteEdges F /(e, ⋯)

theorem Graph.IsLink.contract_contract_comm_of_ne {α : Type u_1} {β : Type u_2} {x y u v : α} {e f : β} {G : Graph α β} [DecidableEq α] (he : G.IsLink e x y) (hf : G.IsLink f u v) (hyv : y ≠ v) (hor : x ≠ v ∨ y ≠ u) (hef : e ≠ f) : G /(e, he) /(f, ⋯) = G /(f, hf) /(e, ⋯)

class Graph.IsPartitionGraph {α : Type u_1} {β : Type u_2} [Order.Frame α] (G : Graph α β) : Prop

• exists_partition : ∃ (P : Partition α), G.vertexSet = P.parts

theorem Graph.exists_partition {α : Type u_1} {β : Type u_2} [Order.Frame α] (G : Graph α β) [h : G.IsPartitionGraph] : ∃ (P : Partition α), G.vertexSet = P.parts

theorem Graph.isPartitionGraph_of_vertex_subset {α : Type u_1} {β : Type u_2} {G H : Graph α β} [Order.Frame α] (h : G.vertexSet ⊆ H.vertexSet) [H.IsPartitionGraph] : G.IsPartitionGraph

theorem Graph.isPartitionGraph_of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} [Order.Frame α] (h : G ≤ H) [H.IsPartitionGraph] : G.IsPartitionGraph

instance Graph.instIsPartitionGraphDeleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} [Order.Frame α] [G.IsPartitionGraph] : (G.deleteVerts X).IsPartitionGraph

instance Graph.instIsPartitionGraphRestrict {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} [Order.Frame α] [G.IsPartitionGraph] : (G.restrict F).IsPartitionGraph

instance Graph.instIsPartitionGraphDeleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} [Order.Frame α] [G.IsPartitionGraph] : (G.deleteEdges F).IsPartitionGraph

def Graph.sContract {α : Type u_1} {β : Type u_2} [Order.Frame α] (G : Graph α β) [G.IsPartitionGraph] (C : Set β) : Graph α β

Equations

• G /[C] = G /[C, fun (x : α) => sSup ((G.restrict C).connPartition.partOf x)]

@[simp]

theorem Graph.sContract_isLink {α : Type u_1} {β : Type u_2} [Order.Frame α] (G : Graph α β) [G.IsPartitionGraph] (C : Set β) (e : β) (x y : α) : G /[C].IsLink e x y = ((∃ (x_1 : α) (y_1 : α), G.IsLink e x_1 y_1 ∧ x = sSup ((G.restrict C).connPartition.partOf x_1) ∧ y = sSup ((G.restrict C).connPartition.partOf y_1)) ∧ e ∉ C)

@[simp]

theorem Graph.vertexSet_sContract {α : Type u_1} {β : Type u_2} [Order.Frame α] (G : Graph α β) [G.IsPartitionGraph] (C : Set β) : G /[C].vertexSet = (fun (x : α) => sSup ((G.restrict C).connPartition.partOf x)) '' G.vertexSet

@[simp]

theorem Graph.edgeSet_sContract {α : Type u_1} {β : Type u_2} [Order.Frame α] (G : Graph α β) [G.IsPartitionGraph] (C : Set β) : G /[C].edgeSet = G.edgeSet \ C

def Graph.«term_/[_]» : Lean.TrailingParserDescr

Equations

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

theorem Graph.sContract_isPartitionGraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : Set β} [Order.Frame α] [G.IsPartitionGraph] : G /[C].IsPartitionGraph

structure Graph.minorMap {α : Type u_1} {β : Type u_2} (G H : Graph α β) : Type (max u_1 u_2)

• map : ↑G.vertexSet → Graph α β
• map_le (x : ↑G.vertexSet) : self.map x ≤ H
• mem_map (x : ↑G.vertexSet) : ↑x ∈ (self.map x).vertexSet
• disj : Pairwise (Function.onFun Disjoint self.map)
• edge_disj (x : ↑G.vertexSet) : Disjoint G.edgeSet (self.map x).edgeSet
• link (e : β) (x y : ↑G.vertexSet) : G.IsLink e ↑x ↑y → ∃ (u : α) (v : α), H.IsLink e u v ∧ u ∈ (self.map x).vertexSet ∧ v ∈ (self.map y).vertexSet
• conn (x : ↑G.vertexSet) : (self.map x).Connected

theorem Graph.minorMap_ext {α : Type u_1} {β : Type u_2} {G H : Graph α β} {F₁ F₂ : G.minorMap H} (hmap : F₁.map = F₂.map) : F₁ = F₂

theorem Graph.minorMap_ext_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} {F₁ F₂ : G.minorMap H} : F₁ = F₂ ↔ F₁.map = F₂.map

@[instance_reducible]

instance Graph.instFunLikeMinorMapElemVertexSet {α : Type u_1} {β : Type u_2} {G H : Graph α β} : FunLike (G.minorMap H) (↑G.vertexSet) (Graph α β)

Equations

• Graph.instFunLikeMinorMapElemVertexSet = { coe := fun (f : G.minorMap H) => f.map, coe_injective := ⋯ }

theorem Graph.minorMap.ne_bot {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) (x : ↑G.vertexSet) : F.map x ≠ ⊥

theorem Graph.minorMap.vertexSet_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) : G.vertexSet ⊆ H.vertexSet

theorem Graph.minorMap.edgeSet_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) : G.edgeSet ⊆ H.edgeSet

theorem Graph.minorMap.disjoint_edgeSet_iUnion {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) : Disjoint G.edgeSet (⋃ (x : ↑G.vertexSet), (F.map x).edgeSet)

theorem Graph.minorMap.mem_iff_eq {α : Type u_1} {β : Type u_2} {y : α} {G H : Graph α β} (F : G.minorMap H) (x : ↑G.vertexSet) (hy : y ∈ (F.map x).vertexSet) : y ∈ G.vertexSet ↔ ↑x = y

theorem Graph.minorMap.inj_of_mem {α : Type u_1} {β : Type u_2} {v : α} {G H : Graph α β} (F : G.minorMap H) {x y : ↑G.vertexSet} (hvx : v ∈ (F.map x).vertexSet) (hvy : v ∈ (F.map y).vertexSet) : x = y

def Graph.minorMap_refl {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.minorMap G

Equations

• G.minorMap_refl = { map := fun (v : ↑G.vertexSet) => Graph.noEdge {↑v} β, map_le := ⋯, mem_map := ⋯, disj := ⋯, edge_disj := ⋯, link := ⋯, conn := ⋯ }

theorem Graph.iUnion_eq_of_forall_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {ι : Type u_7} {Gι : ι → Graph α β} (hG : ∀ (i : ι), Gι i ≤ G) : Graph.iUnion Gι ⋯ = G[⋃ (i : ι), (Gι i).vertexSet].restrict (⋃ (i : ι), (Gι i).edgeSet)

def Graph.minorMap.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G ≤ H) : G.minorMap H

Equations

• Graph.minorMap.of_le h = { map := fun (v : ↑G.vertexSet) => Graph.noEdge {↑v} β, map_le := ⋯, mem_map := ⋯, disj := ⋯, edge_disj := ⋯, link := ⋯, conn := ⋯ }

def Graph.minorMap.of_contract {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : Set β} {φ : α → α} (hφ : (G.restrict C).connPartition.IsRepFun φ) : G /[C, φ].minorMap G

Equations

• Graph.minorMap.of_contract hφ = { map := fun (v : ↑G /[C, φ].vertexSet) => (G.restrict C).walkable ↑v, map_le := ⋯, mem_map := ⋯, disj := ⋯, edge_disj := ⋯, link := ⋯, conn := ⋯ }

def Graph.minorMap.anti_left {α : Type u_1} {β : Type u_2} {G H I : Graph α β} (F : H.minorMap I) (hGH : G ≤ H) : G.minorMap I

Equations

• F.anti_left hGH = { map := fun (v : ↑G.vertexSet) => F.map ⟨↑v, ⋯⟩, map_le := ⋯, mem_map := ⋯, disj := ⋯, edge_disj := ⋯, link := ⋯, conn := ⋯ }

@[simp]

theorem Graph.minorMap.anti_left_map {α : Type u_1} {β : Type u_2} {G H I : Graph α β} (F : H.minorMap I) (hGH : G ≤ H) (v : ↑G.vertexSet) : (F.anti_left hGH).map v = F.map ⟨↑v, ⋯⟩

def Graph.minorMap.mono_right {α : Type u_1} {β : Type u_2} {G H I : Graph α β} (F : G.minorMap H) (hHI : H ≤ I) : G.minorMap I

Equations

• F.mono_right hHI = { map := F.map, map_le := ⋯, mem_map := ⋯, disj := ⋯, edge_disj := ⋯, link := ⋯, conn := ⋯ }

@[simp]

theorem Graph.minorMap.mono_right_map {α : Type u_1} {β : Type u_2} {G H I : Graph α β} (F : G.minorMap H) (hHI : H ≤ I) (a✝ : ↑G.vertexSet) : (F.mono_right hHI).map a✝ = F.map a✝

theorem Graph.minorMap.mem_iUnion_of_edge_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} (F : G.minorMap H) (he : e ∈ G.edgeSet ∪ ⋃ (v : ↑G.vertexSet), (F.map v).edgeSet) (h : H.Inc e x) : x ∈ ⋃ (v : ↑G.vertexSet), (F.map v).vertexSet

def Graph.minorMap.intermediate {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) : Graph α β

Equations

• F.intermediate = H[⋃ (x : ↑G.vertexSet), (F.map x).vertexSet].restrict (G.edgeSet ∪ ⋃ (x : ↑G.vertexSet), (F.map x).edgeSet)

@[simp]

theorem Graph.minorMap.vertexSet_intermediate {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) : F.intermediate.vertexSet = ⋃ (x : ↑G.vertexSet), (F.map x).vertexSet

@[simp]

theorem Graph.minorMap.edgeSet_intermediate {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) : F.intermediate.edgeSet = G.edgeSet ∪ ⋃ (x : ↑G.vertexSet), (F.map x).edgeSet

theorem Graph.minorMap.intermediate_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) : F.intermediate ≤ H

theorem Graph.minorMap.vertexSet_subset_intermediate {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) : G.vertexSet ⊆ F.intermediate.vertexSet

theorem Graph.minorMap.edgeSet_subset_intermediate {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) : G.edgeSet ⊆ F.intermediate.edgeSet

theorem Graph.minorMap.map_isCompOf_intermediate {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) (v : ↑G.vertexSet) : (F.map v).IsCompOf (F.intermediate.restrict (⋃ (x : ↑G.vertexSet), (F.map x).edgeSet))

noncomputable def Graph.minorMap.repFun {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) : α → α

Equations

• F.repFun x = if h : ∃ (v : ↑G.vertexSet), x ∈ (F.map v).vertexSet then ↑h.choose else x

theorem Graph.minorMap.repFun_of_mem_map {α : Type u_1} {β : Type u_2} {v : α} {G H : Graph α β} (F : G.minorMap H) {x : ↑G.vertexSet} (hx : v ∈ (F.map x).vertexSet) : F.repFun v = ↑x

theorem Graph.minorMap.repFun_of {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) (x : ↑G.vertexSet) : F.repFun ↑x = ↑x

theorem Graph.minorMap.repFun_mapsTo {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) : Set.MapsTo F.repFun F.intermediate.vertexSet G.vertexSet

theorem Graph.minorMap.repFun_prop {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) (x : α) (hx : x ∈ F.intermediate.vertexSet) : x ∈ (F.map ⟨F.repFun x, ⋯⟩).vertexSet

theorem Graph.minorMap.repFun_isRepFun {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) : (F.intermediate.restrict (⋃ (x : ↑G.vertexSet), (F.map x).edgeSet)).connPartition.IsRepFun F.repFun

@[simp]

theorem Graph.minorMap.intermediate_isLink {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} (F : G.minorMap H) : F.intermediate.IsLink e x y ↔ H.IsLink e x y ∧ e ∈ G.edgeSet ∪ ⋃ (x : ↑G.vertexSet), (F.map x).edgeSet

theorem Graph.minorMap.eq_contract_of_intermediate {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) : G = F.intermediate /[⋃ (x : ↑G.vertexSet), (F.map x).edgeSet, F.repFun]

theorem Graph.nonempty_minorMap_iff_exists_le_contract {α : Type u_1} {β : Type u_2} (G H : Graph α β) : Nonempty (G.minorMap H) ↔ ∃ (H' : Graph α β) (C : Set β) (φ : α → α), H' ≤ H ∧ (H'.restrict C).connPartition.IsRepFun φ ∧ G = H' /[C, φ]

theorem Graph.minorMap.le_contract_repFun {α : Type u_1} {β : Type u_2} {G H : Graph α β} (F : G.minorMap H) : G ≤ H /[⋃ (x : ↑G.vertexSet), (F.map x).edgeSet, F.repFun]

def Graph.IsMinor {α : Type u_1} {β : Type u_2} (G H : Graph α β) : Prop

Equations

• (G ≤m H) = Nonempty (G.minorMap H)

def Graph.«term_≤m_» : Lean.TrailingParserDescr

Equations

• Graph.«term_≤m_» = Lean.ParserDescr.trailingNode `Graph.«term_≤m_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤m ") (Lean.ParserDescr.cat `term 0))

theorem Graph.IsMinor.refl {α : Type u_1} {β : Type u_2} (G : Graph α β) : G ≤m G

@[simp]

theorem Graph.IsSubgraph.isMinor {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G ≤ H) : G ≤m H

@[simp]

theorem Graph.isMinor_of_contract {α : Type u_1} {β : Type u_2} {G H : Graph α β} {φ : α → α} (hφ : (G.restrict H.edgeSet).connPartition.IsRepFun φ) : G /[H.edgeSet, φ] ≤m G

theorem Graph.IsMinor.vertexSet_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hGH : G ≤m H) : G.vertexSet ⊆ H.vertexSet

theorem Graph.IsMinor.edgeSet_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hGH : G ≤m H) : G.edgeSet ⊆ H.edgeSet