def Graph.ofPFun {α : Type u_1} {β : Type u_2} (f : β →. Sym2 α) : Graph α β

Equations

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

@[simp]

theorem Graph.ofPFun_isLink {α : Type u_1} {β : Type u_2} (f : β →. Sym2 α) (e : β) (x y : α) : (ofPFun f).IsLink e x y = (f e = ↑(some s(x, y)))

@[simp]

theorem Graph.vertexSet_ofPFun {α : Type u_1} {β : Type u_2} (f : β →. Sym2 α) : (ofPFun f).vertexSet = {x : α | ∃ (y : α) (e : β), f e = ↑(some s(x, y))}

@[simp]

theorem Graph.edgeSet_ofPFun {α : Type u_1} {β : Type u_2} (f : β →. Sym2 α) : (ofPFun f).edgeSet = f.Dom

def Graph.map {α : Type u_1} {β : Type u_2} {α' : Type u_3} (f : α → α') (G : Graph α β) : Graph α' β

Map G : Graph α β to a Graph α' β with the same edge set by applying a function f : α → α' to each vertex. Edges between identified vertices become loops.

Equations

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

@[simp]

theorem Graph.edgeSet_map {α : Type u_1} {β : Type u_2} {α' : Type u_3} (f : α → α') (G : Graph α β) : (map f G).edgeSet = G.edgeSet

@[simp]

theorem Graph.vertexSet_map {α : Type u_1} {β : Type u_2} {α' : Type u_3} (f : α → α') (G : Graph α β) : (map f G).vertexSet = f '' G.vertexSet

@[simp]

theorem Graph.map_isLink {α : Type u_1} {β : Type u_2} {α' : Type u_3} (f : α → α') (G : Graph α β) (e : β) (x' y' : α') : (map f G).IsLink e x' y' = ∃ (x : α) (y : α), G.IsLink e x y ∧ x' = f x ∧ y' = f y

def Graph.«term_''ᴳ_» : Lean.TrailingParserDescr

Equations

• Graph.«term_''ᴳ_» = Lean.ParserDescr.trailingNode `Graph.«term_''ᴳ_» 51 52 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ''ᴳ ") (Lean.ParserDescr.cat `term 52))

@[simp]

theorem Graph.map_inc {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {α' : Type u_3} {f : α → α'} {x : α'} : (map f G).Inc e x ↔ ∃ (v : α), G.Inc e v ∧ x = f v

Map has the expected incidence predicate.

@[simp]

theorem Graph.vertexSet_map_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} {α' : Type u_3} {f : α → α'} (h : X ⊆ G.vertexSet) : f '' X ⊆ (map f G).vertexSet

theorem Graph.IsLink.map {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} {α' : Type u_3} (h : G.IsLink e u v) (f : α → α') : (Graph.map f G).IsLink e (f u) (f v)

@[simp]

theorem Graph.map_isLoopAt {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {α' : Type u_3} {f : α → α'} {x : α'} : (map f G).IsLoopAt e x ↔ ∃ (u : α) (v : α), G.IsLink e u v ∧ x = f u ∧ x = f v

theorem Graph.map_congr_left_of_eqOn {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {f g : α → α'} (h : Set.EqOn f g G.vertexSet) : map f G = map g G

@[simp]

theorem Graph.map_id {α : Type u_1} {β : Type u_2} {G : Graph α β} : map id G = G

@[simp]

theorem Graph.map_map {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {g : α → α'} {α'' : Type u_5} {f : α' → α''} : map f (map g G) = map (f ∘ g) G

theorem Graph.eq_map_of_forall_isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {H : Graph α' β} {φ : α → α'} (hf : Set.InjOn φ G.vertexSet) (hV : φ '' G.vertexSet = H.vertexSet) (hE : H.edgeSet ⊆ G.edgeSet) (h : ∀ (e : β) (x y : α), G.IsLink e x y → H.IsLink e (φ x) (φ y)) : map φ G = H

To prove that H is an image of G, it suffices to show some set containments, and mapping links in one direction.

theorem Graph.Compatible.map {α : Type u_1} {β : Type u_2} {G H : Graph α β} {α' : Type u_3} {f : α → α'} (h : G.Compatible H) : (Graph.map f G).Compatible (Graph.map f H)

theorem Graph.map_union {α : Type u_1} {β : Type u_2} {α' : Type u_3} (G H : Graph α β) (f : α → α') : map f (G ∪ H) = map f G ∪ map f H

theorem Graph.map_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} {α' : Type u_3} {f : α → α'} (h : G ≤ H) : map f G ≤ map f H

@[simp]

theorem Graph.map_eq_bot_iff {α : Type u_1} {β : Type u_2} {α' : Type u_3} (G : Graph α β) (φ : α → α') : map φ G = ⊥ ↔ G = ⊥

@[simp]

theorem Graph.map_noEdge {α : Type u_1} {α' : Type u_3} (V : Set α) (β : Type u_5) (φ : α → α') : map φ (noEdge V β) = noEdge (φ '' V) β

theorem Graph.map_isSpanningSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {α' : Type u_3} {f : α → α'} (hsle : G ≤s H) : map f G ≤s map f H

theorem Graph.map_restrict_comm {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {α' : Type u_3} {f : α → α'} : map f (G.restrict F) = (map f G).restrict F

theorem Graph.map_deleteEdges_comm {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {α' : Type u_3} {f : α → α'} : map f (G.deleteEdges F) = (map f G).deleteEdges F

theorem Graph.Adj.map {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {x y : α} (hG : G.Adj x y) (φ : α → α') : (Graph.map φ G).Adj (φ x) (φ y)

theorem Graph.map_adj_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {φ : α → α'} {x y : α'} : (map φ G).Adj x y ↔ ∃ (x₀ : α) (y₀ : α), G.Adj x₀ y₀ ∧ φ x₀ = x ∧ φ y₀ = y

theorem Graph.map_adj_iff_of_injective {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {φ : α → α'} {x y : α} (hφ : Function.Injective φ) : (map φ G).Adj (φ x) (φ y) ↔ G.Adj x y

theorem Graph.map_adj_iff_of_injOn {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {φ : α → α'} {x y : α} (hφ : Set.InjOn φ G.vertexSet) (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) : (map φ G).Adj (φ x) (φ y) ↔ G.Adj x y

theorem Graph.IsComplete.map {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.IsComplete) {α' : Type u_5} (φ : α → α') : (Graph.map φ G).IsComplete

theorem Graph.isComplete_map_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {φ : α → α'} (hφ : Set.InjOn φ G.vertexSet) : (map φ G).IsComplete ↔ G.IsComplete

@[simp]

theorem Graph.IsWalk.map {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {w : WList α β} (f : α → α') (hw : G.IsWalk w) : (Graph.map f G).IsWalk (WList.map f w)

theorem Graph.IsWalk.map_invFunOn {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {f : α → α'} [Nonempty α] (hf : Set.InjOn f G.vertexSet) {w : WList α' β} (hw : (Graph.map f G).IsWalk w) : G.IsWalk (WList.map (Function.invFunOn f G.vertexSet) w)

theorem Graph.IsWalk.map_invFunOn_map {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {f : α → α'} [Nonempty α] {w : WList α' β} (hw : (Graph.map f G).IsWalk w) : WList.map f (WList.map (Function.invFunOn f G.vertexSet) w) = w

@[simp]

theorem Graph.IsTrail.map {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {w : WList α β} (f : α → α') (hw : G.IsTrail w) : (Graph.map f G).IsTrail (WList.map f w)

@[simp]

theorem Graph.IsTour.map {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {w : WList α β} (f : α → α') (hw : G.IsTour w) : (Graph.map f G).IsTour (WList.map f w)

@[simp]

theorem Graph.IsPath.map {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {f : α → α'} {w : WList α β} (hf : Set.InjOn f w.vertexSet) (hw : G.IsPath w) : (Graph.map f G).IsPath (WList.map f w)

@[simp]

theorem Graph.IsCyclicWalk.map {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {f : α → α'} {w : WList α β} (hf : Set.InjOn f w.vertexSet) (hw : G.IsCyclicWalk w) : (Graph.map f G).IsCyclicWalk (WList.map f w)

theorem Graph.IsCyclicWalk.exists_of_map_of_injOn {α : Type u_1} {β : Type u_2} {H : Graph α β} {α' : Type u_3} {φ : α → α'} (hφ : Set.InjOn φ H.vertexSet) {C : WList α' β} (hC : (Graph.map φ H).IsCyclicWalk C) : ∃ (C₀ : WList α β), H.IsCyclicWalk C₀ ∧ WList.map φ C₀ = C

theorem Graph.induce_map_isSpanningSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} {α' : Type u_3} {f : α → α'} : map f G[X] ≤s (map f G)[f '' X]

theorem Graph.map_deleteVerts_isInducedSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} {α' : Type u_3} {f : α → α'} : ((map f G).deleteVerts (f '' X)).IsInducedSubgraph (map f (G.deleteVerts X))

@[simp]

theorem Graph.map_deleteVerts_preimage {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {f : α → α'} {X : Set α'} : map f (G.deleteVerts (f ⁻¹' X)) = (map f G).deleteVerts X

theorem Graph.map_deleteVerts_of_injOn {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {f : α → α'} {X : Set α} (hf : Set.InjOn f G.vertexSet) (hX : X ⊆ G.vertexSet) : map f (G.deleteVerts X) = (map f G).deleteVerts (f '' X)

theorem Graph.map_deleteVerts_of_injective {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {f : α → α'} {X : Set α} (hf : Function.Injective f) : map f (G.deleteVerts X) = (map f G).deleteVerts (f '' X)

@[simp]

theorem Graph.induce_preimage_map {α : Type u_1} {β : Type u_2} {H : Graph α β} {α' : Type u_3} {f : α → α'} {X : Set α'} (h : X ⊆ f '' H.vertexSet) : map f H[f ⁻¹' X] = (map f H)[X]

theorem Graph.surjOn_of_le_map {α : Type u_1} {β : Type u_2} {H : Graph α β} {α' : Type u_3} {f : α → α'} {G : Graph α' β} (h : G ≤ map f H) : Set.SurjOn f H.vertexSet G.vertexSet

theorem Graph.exists_map_eq_of_le_map {α : Type u_1} {β : Type u_2} {H : Graph α β} {α' : Type u_3} {f : α → α'} {G : Graph α' β} (h : G ≤ map f H) : ∃ H' ≤ H, map f H' = G

theorem Graph.exists_le_map_comm {α : Type u_1} {β : Type u_2} {H : Graph α β} {α' : Type u_3} {G : Graph α' β} (f : α → α') : G ≤ map f H ↔ ∃ H' ≤ H, map f H' = G

IsContractClosed predicate

Similar to how combining injecitivity and surjectivity gives a bijection, IsContractClosed is one half of predicate that ensures that contract is sound.

IsContractClosed G φ C means that φ identifies the endpoints of every edge in C. So each fiber of φ is a closed subgraph of G ↾ C.

Notice that each fiber may not be the components of G ↾ C. However, it is sometime useful to use this half-predicate in proofs since it is well-behaved under subgraphs and subsets of C.

def Graph.IsContractClosed {α : Type u_1} {β : Type u_2} {α' : Type u_3} (G : Graph α β) (φ : α → α') (C : Set β) : Prop

Equations

• G.IsContractClosed φ C = ∀ ⦃e : β⦄ ⦃u v : α⦄, e ∈ C → G.IsLink e u v → φ u = φ v

theorem Graph.IsContractClosed.subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_5} {φ : α → α'} {C D : Set β} (hφ : G.IsContractClosed φ C) (hDC : D ⊆ C) : G.IsContractClosed φ D

theorem Graph.IsContractClosed.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {α' : Type u_5} {φ : α → α'} {C : Set β} (hGH : G ≤ H) (hφ : H.IsContractClosed φ C) : G.IsContractClosed φ C

theorem Graph.IsContractClosed.isLoopAt_map_of_mem {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} {α' : Type u_5} {φ : α → α'} {C : Set β} (hφ : G.IsContractClosed φ C) (heC : e ∈ C) (huv : G.IsLink e u v) : (map φ G).IsLoopAt e (φ u)

theorem Graph.IsContractClosed.exists_isLoopAt_map_of_mem_edgeSet {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {α' : Type u_5} {φ : α → α'} {C : Set β} (hφ : G.IsContractClosed φ C) (he : e ∈ C ∩ G.edgeSet) : ∃ (x : α'), (map φ G).IsLoopAt e x

Under IsContractClosed, every edge in C becomes a loop after mapping.

theorem Graph.IsContractClosed.exists_isLoopAt_map_deleteVerts_of_mem {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {α' : Type u_5} {φ : α → α'} {C : Set β} (hφ : G.IsContractClosed φ C) (S : Set α') (he : e ∈ C ∩ ((map φ G).deleteVerts S).edgeSet) : ∃ (x : α'), ((map φ G).deleteVerts S).IsLoopAt e x

A vertex-deletion-stable version: if e ∈ C and e survives deleting S from the mapped graph, then e is a loop in ((φ ''ᴳ G) - S).

theorem Graph.IsContractClosed.disjoint_of_isWalk_noLoop {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_5} {φ : α → α'} {C : Set β} (hφ : G.IsContractClosed φ C) {W : WList α' β} (h : (map φ G).IsWalk W) (hloop : W.NoLoop) : Disjoint W.edgeSet C

theorem Graph.IsContractClosed.exists_isLoopAt_of_isWalk {α : Type u_1} {β : Type u_2} {G : Graph α β} {W : WList α β} {α' : Type u_5} {φ : α → α'} {C : Set β} (hφ : G.IsContractClosed φ C) (hw : G.IsWalk W) (e : β) : e ∈ (WList.map φ W).edge → e ∈ C → ∃ (x : α'), (map φ G).IsLoopAt e x

noncomputable def Graph.edgePreimg {α : Type u_1} {β : Type u_2} {β' : Type u_5} (G : Graph α β) (σ : β' → β) : Graph α β'

Equations

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

@[simp]

theorem Graph.edgeSet_edgePreimg {α : Type u_1} {β : Type u_2} {β' : Type u_5} (G : Graph α β) (σ : β' → β) : (G.edgePreimg σ).edgeSet = σ ⁻¹' G.edgeSet

@[simp]

theorem Graph.edgePreimg_isLink {α : Type u_1} {β : Type u_2} {β' : Type u_5} (G : Graph α β) (σ : β' → β) (e : β') (x y : α) : (G.edgePreimg σ).IsLink e x y = ∃ (e' : β), σ e = e' ∧ G.IsLink e' x y

@[simp]

theorem Graph.vertexSet_edgePreimg {α : Type u_1} {β : Type u_2} {β' : Type u_5} (G : Graph α β) (σ : β' → β) : (G.edgePreimg σ).vertexSet = G.vertexSet

@[simp]

theorem Graph.edgePreimg_inc {α : Type u_1} {β : Type u_2} {u : α} {G : Graph α β} {β' : Type u_5} {e' : β'} {σ : β' → β} : (G.edgePreimg σ).Inc e' u ↔ ∃ (e : β), σ e' = e ∧ G.Inc e u

def Graph.tacticEdgeMap_tac : Lean.ParserDescr

A tactic for providing the proof required in edgeMap in the case where the function is known to be injective on the edge set.

Equations

• Graph.tacticEdgeMap_tac = Lean.ParserDescr.node `Graph.tacticEdgeMap_tac 1024 (Lean.ParserDescr.nonReservedSymbol "edgeMap_tac" false)

def Graph.edgeMap {α : Type u_1} {β : Type u_2} {β' : Type u_6} (G : Graph α β) (σ : β → β') (hσ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, σ e₁ = σ e₂ → G.IsLink e₁ = G.IsLink e₂ := by edgeMap_tac) : Graph α β'

The assumption hσ is needed for an edge-map to be well-defined without choice. It holds in particular if InjOn σ E(G), and the autoParam will prove it if this is known. simps doesn't play nice with the autoParam, so the simp lemms are proved manually.

Equations

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

@[simp]

theorem Graph.edgeMap_isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_6} {e : β'} {x y : α} {σ : β → β'} {hσ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, σ e₁ = σ e₂ → G.IsLink e₁ = G.IsLink e₂} : (G.edgeMap σ hσ).IsLink e x y ↔ ∃ (e' : β), σ e' = e ∧ G.IsLink e' x y

@[simp]

theorem Graph.vertexSet_edgeMap {α : Type u_1} {β : Type u_2} {β' : Type u_6} (G : Graph α β) (σ : β → β') {hσ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, σ e₁ = σ e₂ → G.IsLink e₁ = G.IsLink e₂} : (G.edgeMap σ hσ).vertexSet = G.vertexSet

@[simp]

theorem Graph.edgeSet_edgeMap {α : Type u_1} {β : Type u_2} {β' : Type u_6} (G : Graph α β) (σ : β → β') {hσ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, σ e₁ = σ e₂ → G.IsLink e₁ = G.IsLink e₂} : (G.edgeMap σ hσ).edgeSet = σ '' G.edgeSet

@[simp]

theorem Graph.edgeMap_inc {α : Type u_1} {β : Type u_2} {u : α} {G : Graph α β} {β' : Type u_6} {σ : β → β'} {e' : β'} (hσ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, σ e₁ = σ e₂ → G.IsLink e₁ = G.IsLink e₂) : (G.edgeMap σ hσ).Inc e' u ↔ ∃ (e : β), σ e = e' ∧ G.Inc e u

@[simp]

theorem Graph.edgeMap_isLoopAt {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_6} {σ : β → β'} {e : β'} {x : α} {hσ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, σ e₁ = σ e₂ → G.IsLink e₁ = G.IsLink e₂} : (G.edgeMap σ hσ).IsLoopAt e x ↔ ∃ (f : β), σ f = e ∧ G.IsLoopAt f x

@[simp]

theorem Graph.edgeMap_isNonloopAt {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_6} {σ : β → β'} {e : β'} {x : α} {hσ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, σ e₁ = σ e₂ → G.IsLink e₁ = G.IsLink e₂} : (G.edgeMap σ hσ).IsNonloopAt e x ↔ ∃ (f : β), σ f = e ∧ G.IsNonloopAt f x

@[simp]

theorem Graph.edgeMap_noEdge {α : Type u_1} (V : Set α) {β : Type u_7} {β' : Type u_8} {σ : β → β'} {hσ : ∀ e₁ ∈ (noEdge V β).edgeSet, ∀ e₂ ∈ (noEdge V β).edgeSet, σ e₁ = σ e₂ → (noEdge V β).IsLink e₁ = (noEdge V β).IsLink e₂} : (noEdge V β).edgeMap σ hσ = noEdge V β'

theorem Graph.IsLink.edgeMap {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {x y : α} {β' : Type u_6} (h : G.IsLink e x y) (φ : β → β') (hφ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, φ e₁ = φ e₂ → G.IsLink e₁ = G.IsLink e₂) : (G.edgeMap φ hφ).IsLink (φ e) x y

@[simp]

theorem Graph.edgeMap_adj_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {β' : Type u_6} {φ : β → β'} {hφ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, φ e₁ = φ e₂ → G.IsLink e₁ = G.IsLink e₂} : (G.edgeMap φ hφ).Adj x y ↔ G.Adj x y

theorem Graph.edgeMap_adj_eq {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_6} {φ : β → β'} {hφ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, φ e₁ = φ e₂ → G.IsLink e₁ = G.IsLink e₂} : (G.edgeMap φ hφ).Adj = G.Adj

@[simp]

theorem Graph.isComplete_edgeMap_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_6} {φ : β → β'} {hφ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, φ e₁ = φ e₂ → G.IsLink e₁ = G.IsLink e₂} : (G.edgeMap φ hφ).IsComplete ↔ G.IsComplete

@[simp]

theorem Graph.edgeMap_eq_bot_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_6} {φ : β → β'} {hφ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, φ e₁ = φ e₂ → G.IsLink e₁ = G.IsLink e₂} : G.edgeMap φ hφ = ⊥ ↔ G = ⊥

@[simp]

theorem Graph.edgeMap_deleteVerts {α : Type u_1} {β : Type u_2} {β' : Type u_6} (G : Graph α β) {φ : β → β'} (hφ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, φ e₁ = φ e₂ → G.IsLink e₁ = G.IsLink e₂) (X : Set α) : (G.deleteVerts X).edgeMap φ ⋯ = (G.edgeMap φ hφ).deleteVerts X

@[simp]

theorem Graph.IsWalk.edgeMap {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {β' : Type u_6} (hw : G.IsWalk w) (σ : β → β') (hσ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, σ e₁ = σ e₂ → G.IsLink e₁ = G.IsLink e₂) : (G.edgeMap σ hσ).IsWalk (WList.edgeMap σ w)

theorem Graph.IsWalk.edgeMap_invFunOn {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_6} {σ : β → β'} [Nonempty β] {w : WList α β'} {hσ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, σ e₁ = σ e₂ → G.IsLink e₁ = G.IsLink e₂} (hw : (G.edgeMap σ hσ).IsWalk w) (hinj : Set.InjOn σ G.edgeSet) : G.IsWalk (WList.edgeMap (Function.invFunOn σ G.edgeSet) w)

theorem Graph.IsWalk.edgeMap_invFunOn_edgeMap {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_6} {σ : β → β'} [Nonempty β] {w : WList α β'} {hσ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, σ e₁ = σ e₂ → G.IsLink e₁ = G.IsLink e₂} (hw : (G.edgeMap σ hσ).IsWalk w) (hinj : Set.InjOn σ G.edgeSet) : WList.edgeMap σ (WList.edgeMap (Function.invFunOn σ G.edgeSet) w) = w

@[simp]

theorem Graph.IsTrail.edgeMap {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {β' : Type u_6} (hw : G.IsTrail w) (σ : β → β') (hσ : Set.InjOn σ G.edgeSet) : (G.edgeMap σ ⋯).IsTrail (WList.edgeMap σ w)

@[simp]

theorem Graph.IsTour.edgeMap {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {β' : Type u_6} (hw : G.IsTour w) (σ : β → β') (hσ : Set.InjOn σ G.edgeSet) : (G.edgeMap σ ⋯).IsTour (WList.edgeMap σ w)

@[simp]

theorem Graph.IsPath.edgeMap {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {β' : Type u_6} (hw : G.IsPath w) (σ : β → β') (hσ : Set.InjOn σ G.edgeSet) : (G.edgeMap σ ⋯).IsPath (WList.edgeMap σ w)

@[simp]

theorem Graph.IsCyclicWalk.edgeMap {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {β' : Type u_6} (hw : G.IsCyclicWalk w) (σ : β → β') (hσ : Set.InjOn σ G.edgeSet) : (G.edgeMap σ ⋯).IsCyclicWalk (WList.edgeMap σ w)

theorem Graph.IsCyclicWalk.exists_of_edgeMap_of_injOn {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_6} {σ : β → β'} (hσ : Set.InjOn σ G.edgeSet) {C : WList α β'} (hC : (G.edgeMap σ ⋯).IsCyclicWalk C) : ∃ (C₀ : WList α β), G.IsCyclicWalk C₀ ∧ WList.edgeMap σ C₀ = C

theorem Graph.eq_edgeMap_of_forall_isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_7} {H : Graph α β'} {φ : β → β'} (hφ : Set.InjOn φ G.edgeSet) (hH : G.vertexSet = H.vertexSet) (hss : H.edgeSet ⊆ φ '' G.edgeSet) (h : ∀ (e : β) (x y : α), G.IsLink e x y → H.IsLink (φ e) x y) : H = G.edgeMap φ ⋯

theorem Graph.eq_edgeMap_of_forall_isLink' {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_7} {H : Graph α β'} {φ : β → β'} (hφ : Set.InjOn φ G.edgeSet) (hV : G.vertexSet = H.vertexSet) (hH : ∀ ⦃e : β'⦄ ⦃x y : α⦄, H.IsLink e x y → ∃ (e' : β), G.IsLink e' x y ∧ φ e' = e) (hG : ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → H.IsLink (φ e) x y) : H = G.edgeMap φ ⋯

theorem Graph.eq_map_edgeMap_of_forall {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_7} {β' : Type u_8} {φ : α → α'} {ψ : β → β'} {H : Graph α' β'} (hψ : Set.InjOn ψ G.edgeSet) (hV : H.vertexSet = φ '' G.vertexSet) (hG : ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → H.IsLink (ψ e) (φ x) (φ y)) (hH : ∀ ⦃e : β'⦄ ⦃x y : α'⦄, H.IsLink e x y → ∃ (e' : β) (x' : α) (y' : α), G.IsLink e' x' y' ∧ ψ e' = e) : H = (map φ G).edgeMap ψ ⋯

If φ and ψ are functions out of the vertex and edge sets respectively, a sufficient condition for a graph H to be a map of G by φ and ψ. This will only apply if φ and ψ give an isomorphism from G to H.

theorem Graph.eq_map_edgeMap_of_forall_inc {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_7} {β' : Type u_8} {φ : α → α'} {ψ : β → β'} {H : Graph α' β'} (hψ : Set.InjOn ψ G.edgeSet) (hV : H.vertexSet = φ '' G.vertexSet) (hG : ∀ ⦃e : β⦄ ⦃x : α⦄, G.Inc e x → H.Inc (ψ e) (φ x)) (hH : ∀ ⦃e : β'⦄ ⦃x : α'⦄, H.Inc e x → ∃ (e' : β) (x' : α), G.Inc e' x' ∧ φ x' = x ∧ ψ e' = e) : H = (map φ G).edgeMap ψ ⋯

If φ and ψ are functions out of the vertex and edge sets respectively, a sufficient condition for a graph H to be a map of G by φ and ψ. This will only apply if φ and ψ give an isomorphism from G to H.

theorem Graph.setLinkEdges_map_image {α : Type u_1} {β : Type u_2} (G : Graph α β) {S T : Set α} (hS : S ⊆ G.vertexSet) (hT : T ⊆ G.vertexSet) {α' : Type u_7} {φ : α → α'} (hφ : Set.InjOn φ G.vertexSet) : E(map φ G, φ '' S, φ '' T) = E(G, S, T)

theorem Graph.setLinkEdges_map_image_of_injective {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) {α' : Type u_7} {φ : α → α'} (hφ : Function.Injective φ) : E(map φ G, φ '' S, φ '' T) = E(G, S, T)

theorem Graph.setLinkEdges_map {α : Type u_1} {β : Type u_2} (G : Graph α β) {α' : Type u_7} {φ : α → α'} {S T : Set α'} (hφ : Set.InjOn φ G.vertexSet) : E(map φ G, S, T) = E(G, φ ⁻¹' S, φ ⁻¹' T)

@[simp]

theorem Graph.setLinkEdges_edgeMap {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) {β' : Type u_7} {σ : β → β'} {hσ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, σ e₁ = σ e₂ → G.IsLink e₁ = G.IsLink e₂} : E(G.edgeMap σ hσ, S, T) = σ '' E(G, S, T)