Basic Graph Theory

This file extends Mathlib.Combinatorics.Graph.Basic with additional definitions and lemmas for multigraphs with type Graph α β (where α is the vertex type and β is the edge type).

Main definitions

• endSet: The set of endpoints of an edge.
• incVertexSet: The set of vertices incident to a set of edges.
• parallel: Two edges are parallel if they have the same endpoints.
• Neighbor: The (open) neighborhood of a vertex.
• SetNeighbor: The external neighborhood of a set of vertices.
• IncEdges: The set of edges incident to a vertex.
• SetIncEdges: The set of edges incident to a set of vertices.
• LinkEdges: The set of edges linking two vertices.
• SetLinkEdges: The set of edges with endpoints in two given sets.
• Isolated: A vertex with no incident edges.
• IsPendant: An edge that is the unique edge incident to one of its endpoints.
• IsLeaf: A vertex with exactly one incident edge.
• IsLeafEdge: An edge that is pendant at some vertex.

Additional lemmas for Graph

This section contains auxiliary lemmas and definitions for the Graph structure from Mathlib, extending basic graph functionality for use in matroid theory.

@[simp]

theorem Graph.IsLink.other_eq {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : Inc.other ⋯ = y

@[simp]

theorem Graph.IsLoopAt.other_eq {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e x) : ⋯.other = x

@[simp]

theorem Graph.IsNonloopAt.other_ne {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsNonloopAt e x) : ⋯.other ≠ x

@[simp]

theorem Graph.Inc.other_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) : h.other ∈ G.vertexSet

theorem Graph.IsLoopAt.eq_of_isLink {α : Type u_1} {β : Type u_2} {x y v : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e v) (h' : G.IsLink e x y) : v = x ∧ v = y

instance Graph.instSymmAdj_matroid {α : Type u_1} {β : Type u_2} {G : Graph α β} : Std.Symm G.Adj

theorem Graph.isLink_eq_isLink_iff_exists_isLink_of_mem_edgeSet {α : Type u_1} {β : Type u_2} {e : β} {G H : Graph α β} (heG : e ∈ G.edgeSet) : G.IsLink e = H.IsLink e ↔ ∃ (x : α) (y : α), G.IsLink e x y ∧ H.IsLink e x y

Two graphs G and H have the same IsLink function for edge e if and only if there exist vertices x and y such that both graphs agree that e links x and y.

def Graph.endSet {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) : Set α

The set of ends of an edge e.

Equations

• V(G, e) = {x : α | G.Inc e x}

def Graph.«termV(_,_)» : Lean.ParserDescr

Equations

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

@[simp]

theorem Graph.mem_endSet_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} : x ∈ V(G, e) ↔ G.Inc e x

theorem Graph.IsLink.endSet_eq {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : V(G, e) = {x, y}

theorem Graph.IsLoopAt.endSet_eq {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e x) : V(G, e) = {x}

@[simp]

theorem Graph.endSet_eq_of_notMem {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} (he : e ∉ G.edgeSet) : V(G, e) = ∅

theorem Graph.inc_iff_isLoopAt_or_isNonloopAt {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} : G.Inc e x ↔ G.IsLoopAt e x ∨ G.IsNonloopAt e x

@[simp]

theorem Graph.endSet_encard_le_two {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) : V(G, e).encard ≤ 2

def Graph.incVertexSet {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : Set α

The set of vertices incident to at least one edge in F. Also known as the vertex set of the edge set F.

Equations

• V(G, F) = {x : α | ∃ e ∈ F, G.Inc e x}

def Graph.«termV(_,_)_1» : Lean.ParserDescr

Equations

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

@[simp]

theorem Graph.mem_incVertexSet_iff {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {F : Set β} : x ∈ V(G, F) ↔ ∃ e ∈ F, G.Inc e x

@[simp]

theorem Graph.incVertexSet_subset {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : V(G, F) ⊆ G.vertexSet

theorem Graph.incVertexSet_eq_sUnion {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : V(G, F) = ⋃ e ∈ F, V(G, e)

theorem Graph.incVertexSet_encard_le {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : V(G, F).encard ≤ 2 * F.encard

theorem Graph.incVertexSet_inter_edgeSet {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : V(G, F ∩ G.edgeSet) = V(G, F)

noncomputable def Graph.ends {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : ↑G.edgeSet) : Sym2 ↑G.vertexSet

The function mapping an edge of G to an unordered pair of its endpoints (as elements of the vertex subtype). Used mostly as an implementation detail.

Equations

• G.ends e = s(⟨⋯.choose, ⋯⟩, ⟨⋯.choose, ⋯⟩)

theorem Graph.IsLink.ends_eq {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : G.ends ⟨e, ⋯⟩ = s(⟨x, ⋯⟩, ⟨y, ⋯⟩)

theorem Graph.IsNonloopAt.vertexSet_nontrivial {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsNonloopAt e x) : G.vertexSet.Nontrivial

theorem Graph.inc_eq_inc_iff {α : Type u_1} {β : Type u_2} {e f : β} {G₁ G₂ : Graph α β} : G₁.Inc e = G₂.Inc f ↔ G₁.IsLink e = G₂.IsLink f

def Graph.parallel {α : Type u_1} {β : Type u_2} (G : Graph α β) (e f : β) : Prop

Two edges e and f are parallel in G if they are both in the edge set of G and have the same endpoints (i.e., the same IsLink function).

Equations

• G.parallel e f = (e ∈ G.edgeSet ∧ f ∈ G.edgeSet ∧ G.IsLink e = G.IsLink f)

theorem Graph.parallel.left_mem {α : Type u_1} {β : Type u_2} {e f : β} {G : Graph α β} (h : G.parallel e f) : e ∈ G.edgeSet

theorem Graph.parallel.right_mem {α : Type u_1} {β : Type u_2} {e f : β} {G : Graph α β} (h : G.parallel e f) : f ∈ G.edgeSet

theorem Graph.parallel.isLink_eq {α : Type u_1} {β : Type u_2} {e f : β} {G : Graph α β} (h : G.parallel e f) : G.IsLink e = G.IsLink f

@[simp]

theorem Graph.parallel_refl {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} (he : e ∈ G.edgeSet) : G.parallel e e

@[simp]

theorem Graph.parallel_refl_iff {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} : G.parallel e e ↔ e ∈ G.edgeSet

theorem Graph.parallel_iff_inc_eq {α : Type u_1} {β : Type u_2} (G : Graph α β) (e f : β) : G.parallel e f ↔ e ∈ G.edgeSet ∧ f ∈ G.edgeSet ∧ G.Inc e = G.Inc f

theorem Graph.inc_eq_inc_iff_parallel {α : Type u_1} {β : Type u_2} (G : Graph α β) {e f : β} (he : e ∈ G.edgeSet) (hf : f ∈ G.edgeSet) : G.Inc e = G.Inc f ↔ G.parallel e f

theorem Graph.parallel.inc_eq {α : Type u_1} {β : Type u_2} {e f : β} {G : Graph α β} (h : G.parallel e f) : G.Inc e = G.Inc f

theorem Graph.parallel.symm {α : Type u_1} {β : Type u_2} {e f : β} {G : Graph α β} (h : G.parallel e f) : G.parallel f e

instance Graph.instSymmParallel {α : Type u_1} {β : Type u_2} {G : Graph α β} : Std.Symm G.parallel

theorem Graph.parallel_comm {α : Type u_1} {β : Type u_2} {e f : β} {G : Graph α β} : G.parallel e f ↔ G.parallel f e

theorem Graph.parallel.trans {α : Type u_1} {β : Type u_2} {e f : β} {G : Graph α β} {g : β} (h : G.parallel e f) (h' : G.parallel f g) : G.parallel e g

instance Graph.instIsTransParallel {α : Type u_1} {β : Type u_2} {G : Graph α β} : IsTrans β G.parallel

def Graph.parallelClasses {α : Type u_1} {β : Type u_2} (G : Graph α β) : Partition (Set β)

Equations

• G.parallelClasses = Partition.ofRel G.parallel

@[simp]

theorem Graph.parallelClasses_supp {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.parallelClasses.supp = G.edgeSet

def Graph.Neighbor {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : Set α

The set of vertices adjacent to x in G. Also called the (open) neighborhood of x.

Equations

• N(G, x) = {y : α | G.Adj x y}

def Graph.«termN(_,_)» : Lean.ParserDescr

Equations

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

@[simp]

theorem Graph.neighbor_subset {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : N(G, x) ⊆ G.vertexSet

@[simp]

theorem Graph.notMem_neighbor_of_not_adj {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β} (hadj : ¬G.Adj x y) : y ∉ N(G, x)

theorem Graph.neighbor_subset_of_ne_not_adj {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β} (hne : x ≠ y) (hadj : ¬G.Adj x y) : N(G, x) \ {x} ⊆ G.vertexSet \ {x, y}

def Graph.SetNeighbor {α : Type u_1} {β : Type u_2} (G : Graph α β) (S : Set α) : Set α

The set of vertices outside S that are adjacent to at least one vertex in S. Also called the (external) neighborhood of S.

Equations

• N(G, S) = {y : α | y ∉ S ∧ ∃ x ∈ S, G.Adj x y}

def Graph.«termN(_,_)_1» : Lean.ParserDescr

Equations

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

@[simp]

theorem Graph.setNeighbor_subset {α : Type u_1} {β : Type u_2} (G : Graph α β) (S : Set α) : N(G, S) ⊆ G.vertexSet

@[simp]

theorem Graph.setNeighbor_disjoint {α : Type u_1} {β : Type u_2} (G : Graph α β) (S : Set α) : Disjoint S N(G, S)

@[simp]

theorem Graph.notMem_setNeighbor_of_not_adj {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β} (hadj : ¬G.Adj x y) : y ∉ N(G, {x})

def Graph.IncEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (v : α) : Set β

The set of edges incident to vertex v in G.

Equations

• E(G, v) = {e : β | G.Inc e v}

def Graph.«termE(_,_)» : Lean.ParserDescr

Equations

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

@[simp]

theorem Graph.incEdges_subset {α : Type u_1} {β : Type u_2} (G : Graph α β) (v : α) : E(G, v) ⊆ G.edgeSet

@[simp]

theorem Graph.mem_incEdges_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (v : α) (e : β) : e ∈ E(G, v) ↔ G.Inc e v

def Graph.SetIncEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (S : Set α) : Set β

The set of edges incident to at least one vertex in S.

Equations

• E(G, S) = {e : β | ∃ x ∈ S, G.Inc e x}

def Graph.«termE(_,_)_1» : Lean.ParserDescr

Equations

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

@[simp]

theorem Graph.setIncEdges_subset {α : Type u_1} {β : Type u_2} (G : Graph α β) (S : Set α) : E(G, S) ⊆ G.edgeSet

theorem Graph.setIncEdges_mono_right {α : Type u_1} {β : Type u_2} (G : Graph α β) {S T : Set α} (hST : S ⊆ T) : E(G, S) ⊆ E(G, T)

@[simp]

theorem Graph.setIncEdges_vertexSet {α : Type u_1} {β : Type u_2} (G : Graph α β) : E(G, G.vertexSet) = G.edgeSet

@[simp]

theorem Graph.mem_setIncEdges_iff {α : Type u_1} {β : Type u_2} {e : β} (G : Graph α β) (S : Set α) : e ∈ E(G, S) ↔ ∃ x ∈ S, G.Inc e x

@[simp]

theorem Graph.setIncEdges_singleton {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : E(G, {x}) = E(G, x)

theorem Graph.incEdge_subset_setIncEdges {α : Type u_1} {β : Type u_2} {x : α} (G : Graph α β) {S : Set α} (hx : x ∈ S) : E(G, x) ⊆ E(G, S)

def Graph.LinkEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (u v : α) : Set β

The set of edges linking vertices u and v in G. When u = v, this is the set of loops at u.

Equations

• E(G, u, v) = {e : β | G.IsLink e u v}

def Graph.«termE(_,_,_)» : Lean.ParserDescr

Equations

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

@[simp]

theorem Graph.linkEdges_empty {α : Type u_1} {β : Type u_2} (G : Graph α β) (u v : α) : E(G, u, v) = ∅ ↔ ¬G.Adj u v

@[simp]

theorem Graph.linkEdges_self {α : Type u_1} {β : Type u_2} (G : Graph α β) (u : α) : E(G, u, u) = {e : β | G.IsLoopAt e u}

@[simp]

theorem Graph.mem_linkEdges_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (u v : α) (e : β) : e ∈ E(G, u, v) ↔ G.IsLink e u v

theorem Graph.linkEdges_subset_incEdges_left {α : Type u_1} {β : Type u_2} (G : Graph α β) (u v : α) : E(G, u, v) ⊆ E(G, u)

theorem Graph.linkEdges_subset_incEdges_right {α : Type u_1} {β : Type u_2} (G : Graph α β) (u v : α) : E(G, u, v) ⊆ E(G, v)

@[simp]

theorem Graph.linkEdges_eq_empty_of_left_not_mem {α : Type u_1} {β : Type u_2} {u : α} {G : Graph α β} (hu : u ∉ G.vertexSet) (v : α) : E(G, u, v) = ∅

@[simp]

theorem Graph.linkEdges_eq_empty_of_right_not_mem {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} (u : α) (hv : v ∉ G.vertexSet) : E(G, u, v) = ∅

theorem Graph.linkEdges_comm {α : Type u_1} {β : Type u_2} (G : Graph α β) (u v : α) : E(G, u, v) = E(G, v, u)

def Graph.SetLinkEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : Set β

The set of edges with one endpoint in S and one endpoint in T.

Equations

• E(G, S, T) = {e : β | ∃ x ∈ S, ∃ y ∈ T, G.IsLink e x y}

def Graph.«termE(_,_,_)_1» : Lean.ParserDescr

Equations

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

def Graph.«termδ(_,_)» : Lean.ParserDescr

The edge boundary (or cut) of S: edges with one endpoint in S and one endpoint outside S.

Equations

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

theorem Graph.mem_setLinkEdges_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) (e : β) : e ∈ E(G, S, T) ↔ ∃ x ∈ S, ∃ y ∈ T, G.IsLink e x y

theorem Graph.IsLink.mem_setLinkEdges_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {S T : Set α} (h : G.IsLink e x y) : e ∈ E(G, S, T) ↔ x ∈ S ∧ y ∈ T ∨ x ∈ T ∧ y ∈ S

theorem Graph.setLinkEdges_subset {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : E(G, S, T) ⊆ G.edgeSet

theorem Graph.setLinkEdges_mono_left {α : Type u_1} {β : Type u_2} {S T X : Set α} (G : Graph α β) (hST : S ⊆ X) : E(G, S, T) ⊆ E(G, X, T)

theorem Graph.setLinkEdges_mono_right {α : Type u_1} {β : Type u_2} {S T Y : Set α} (G : Graph α β) (hST : T ⊆ Y) : E(G, S, T) ⊆ E(G, S, Y)

theorem Graph.setLinkEdges_comm {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : E(G, S, T) = E(G, T, S)

theorem Graph.setLinkEdges_vertexSet_inter_left {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : E(G, G.vertexSet ∩ S, T) = E(G, S, T)

theorem Graph.setLinkEdges_vertexSet_inter_right {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : E(G, S, G.vertexSet ∩ T) = E(G, S, T)

theorem Graph.setLinkEdges_subset_setIncEdges_left {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : E(G, S, T) ⊆ E(G, S)

theorem Graph.setLinkEdges_subset_setIncEdges_right {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : E(G, S, T) ⊆ E(G, T)

theorem Graph.setLinkEdges_singleton_eq_setOf_isNonloopAt {α : Type u_1} {β : Type u_2} {G : Graph α β} (v : α) : E(G, {v}, G.vertexSet \ {v}) = {e : β | G.IsNonloopAt e v}

Isolated vertices

An isolated vertex is a vertex that is incident with no edges.

structure Graph.Isolated {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : Prop

An Isolated vertex is one that is incident with no edge but is in the vertex set.

• not_inc ⦃e : β⦄ : ¬G.Inc e x
• mem : x ∈ G.vertexSet

theorem Graph.isolated_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : G.Isolated x ↔ (∀ ⦃e : β⦄, ¬G.Inc e x) ∧ x ∈ G.vertexSet

@[simp]

theorem Graph.Isolated.not_adj {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β} (h : G.Isolated x) : ¬G.Adj x y

@[simp]

theorem Graph.Isolated.not_isLink {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.Isolated x) : ¬G.IsLink e x y

theorem Graph.isolated_or_exists_isLink {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (hx : x ∈ G.vertexSet) : G.Isolated x ∨ ∃ (e : β) (y : α), G.IsLink e x y

def Graph.IsolatedSet {α : Type u_1} {β : Type u_2} (G : Graph α β) : Set α

The set of isolated vertices in G.

Equations

• G.IsolatedSet = {x : α | G.Isolated x}

def Graph.«termIsol(_)» : Lean.ParserDescr

Equations

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

@[simp]

theorem Graph.mem_isolatedSet_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : x ∈ G.IsolatedSet ↔ G.Isolated x

@[simp]

theorem Graph.isolatedSet_subset {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.IsolatedSet ⊆ G.vertexSet

@[simp]

theorem Graph.setincEdges_isolatedSet {α : Type u_1} {β : Type u_2} (G : Graph α β) : E(G, G.IsolatedSet) = ∅

@[simp]

theorem Graph.not_isolated_iff {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} (hv : v ∈ G.vertexSet) : ¬G.Isolated v ↔ ∃ (e : β), G.Inc e v

@[simp]

theorem Graph.incEdges_empty_iff {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} (hv : v ∈ G.vertexSet) : E(G, v) = ∅ ↔ G.Isolated v

@[simp]

theorem Graph.SetIncEdges_empty_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} (hS : S ⊆ G.vertexSet) : E(G, S) = ∅ ↔ S ⊆ G.IsolatedSet

@[simp]

theorem Graph.IsLink.left_not_isolated {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : ¬G.Isolated x

@[simp]

theorem Graph.IsLink.right_not_isolated {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : ¬G.Isolated y

Leaves

A leaf (or degree-one vertex) is a vertex with exactly one incident edge, and that edge is a nonloop. A pendant edge is an edge that is the unique edge incident to one of its endpoints.

structure Graph.IsPendant {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (x : α) : Prop

G.IsPendant e x means that e is a nonloop edge at x, and is the unique edge incident to x.

• isNonloopAt : G.IsNonloopAt e x
• edge_unique ⦃f : β⦄ : G.Inc f x → f = e

theorem Graph.isPendant_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (x : α) : G.IsPendant e x ↔ G.IsNonloopAt e x ∧ ∀ ⦃f : β⦄, G.Inc f x → f = e

theorem Graph.IsPendant.not_isLoopAt {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsPendant e x) (f : β) : ¬G.IsLoopAt f x

theorem Graph.IsPendant.edge_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsPendant e x) : e ∈ G.edgeSet

theorem Graph.IsPendant.vertex_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsPendant e x) : x ∈ G.vertexSet

def Graph.IsLeaf {α : Type u_1} {β : Type u_2} (G : Graph α β) (v : α) : Prop

A leaf (or degree-one vertex) is a vertex that has exactly one incident edge, which is a nonloop.

Equations

• G.IsLeaf v = ∃ (e : β), G.IsPendant e v

theorem Graph.IsPendant.isLeaf {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsPendant e x) : G.IsLeaf x

theorem Graph.IsLeaf.mem {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} (h : G.IsLeaf v) : v ∈ G.vertexSet

theorem Graph.IsLeaf.vertexSet_nontrivial {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} (h : G.IsLeaf v) : G.vertexSet.Nontrivial

theorem Graph.IsLeaf.exists_unique_inc {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (h : G.IsLeaf x) : ∃! e : β, G.Inc e x

theorem Graph.IsLeaf.exists_unique_adj {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (h : G.IsLeaf x) : ∃! y : α, G.Adj x y

theorem Graph.IsLeaf.eq_of_adj_adj {α : Type u_1} {β : Type u_2} {x u v : α} {G : Graph α β} (h : G.IsLeaf x) (hu : G.Adj x u) (hv : G.Adj x v) : u = v

theorem Graph.IsLeaf.eq_of_inc_inc {α : Type u_1} {β : Type u_2} {x : α} {e f : β} {G : Graph α β} (h : G.IsLeaf x) (he : G.Inc e x) (hf : G.Inc f x) : e = f

theorem Graph.IsLeaf.not_adj_self {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (h : G.IsLeaf x) : ¬G.Adj x x

theorem Graph.IsLeaf.ne_of_adj {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β} (h : G.IsLeaf x) (hxy : G.Adj x y) : x ≠ y

theorem Graph.IsLeaf.not_isLoopAt {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (h : G.IsLeaf x) (e : β) : ¬G.IsLoopAt e x

def Graph.IsLeafEdge {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) : Prop

A leaf edge (or pendant edge) is an edge that is the unique edge incident to (at least) one of its endpoints.

Equations

• G.IsLeafEdge e = ∃ (x : α), G.IsPendant e x

def Graph.ofExistsGraph {α : Type u_1} {β : Type u_2} (V : Set α) (E : Set β) (isLink : β → α → α → Prop) (h : ∃ (G : Graph α β), G.vertexSet = V ∧ G.edgeSet = E ∧ ∀ (e : β) (x y : α), isLink e x y ↔ G.IsLink e x y) : Graph α β

Define a graph using another graph. Allows the incidence predicate and vertex/edge sets to be definitionally more convenient.

Equations

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

@[simp]

theorem Graph.vertexSet_ofExistsGraph {α : Type u_1} {β : Type u_2} (V : Set α) (E : Set β) (isLink : β → α → α → Prop) (h : ∃ (G : Graph α β), G.vertexSet = V ∧ G.edgeSet = E ∧ ∀ (e : β) (x y : α), isLink e x y ↔ G.IsLink e x y) : (ofExistsGraph V E isLink h).vertexSet = V

@[simp]

theorem Graph.edgeSet_ofExistsGraph {α : Type u_1} {β : Type u_2} (V : Set α) (E : Set β) (isLink : β → α → α → Prop) (h : ∃ (G : Graph α β), G.vertexSet = V ∧ G.edgeSet = E ∧ ∀ (e : β) (x y : α), isLink e x y ↔ G.IsLink e x y) : (ofExistsGraph V E isLink h).edgeSet = E

@[simp]

theorem Graph.ofExistsGraph_isLink {α : Type u_1} {β : Type u_2} (V : Set α) (E : Set β) (isLink : β → α → α → Prop) (h : ∃ (G : Graph α β), G.vertexSet = V ∧ G.edgeSet = E ∧ ∀ (e : β) (x y : α), isLink e x y ↔ G.IsLink e x y) (a✝ : β) (a✝¹ a✝² : α) : (ofExistsGraph V E isLink h).IsLink a✝ a✝¹ a✝² = isLink a✝ a✝¹ a✝²