theorem Graph.noEdge_not_inc {α : Type u_1} {β : Type u_2} {x : α} {e : β} {V : Set α} : ¬(noEdge V β).Inc e x

@[simp]

theorem Graph.noEdge_not_isLoopAt {α : Type u_1} {β : Type u_2} {x : α} {e : β} {V : Set α} : ¬(noEdge V β).IsLoopAt e x

@[simp]

theorem Graph.noEdge_not_isNonloopAt {α : Type u_1} {β : Type u_2} {x : α} {e : β} {V : Set α} : ¬(noEdge V β).IsNonloopAt e x

@[simp]

theorem Graph.noEdge_not_adj {α : Type u_1} {β : Type u_2} {x y : α} {V : Set α} : ¬(noEdge V β).Adj x y

theorem Graph.edgeSet_eq_empty_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.edgeSet = ∅ ↔ G = noEdge G.vertexSet β

@[simp]

theorem Graph.noEdge_incEdges {α : Type u_1} {β : Type u_2} {x : α} {X : Set α} : E(noEdge X β, x) = ∅

instance Graph.instIsEmptyElemVertexSetBot_matroid {α : Type u_1} {β : Type u_2} : IsEmpty ↑⊥.vertexSet

instance Graph.instIsEmptyElemEdgeSetBot_matroid {α : Type u_1} {β : Type u_2} : IsEmpty ↑⊥.edgeSet

def Graph.singleEdge {α : Type u_1} {β : Type u_2} (u v : α) (e : β) : Graph α β

A graph with a single edge e from u to v

Equations

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

@[simp]

theorem Graph.vertexSet_singleEdge {α : Type u_1} {β : Type u_2} (u v : α) (e : β) : (Graph.singleEdge u v e).vertexSet = {u, v}

@[simp]

theorem Graph.edgeSet_singleEdge {α : Type u_1} {β : Type u_2} (u v : α) (e : β) : (Graph.singleEdge u v e).edgeSet = {e}

@[simp]

theorem Graph.singleEdge_isLink {α : Type u_1} {β : Type u_2} (u v : α) (e e' : β) (x y : α) : (Graph.singleEdge u v e).IsLink e' x y = (e' = e ∧ (x = u ∧ y = v ∨ x = v ∧ y = u))

theorem Graph.singleEdge_comm {α : Type u_1} {β : Type u_2} (u v : α) (e : β) : Graph.singleEdge u v e = Graph.singleEdge v u e

theorem Graph.singleEdge_isLink_iff {α : Type u_1} {β : Type u_2} {x y u v : α} {e f : β} : (Graph.singleEdge u v e).IsLink f x y ↔ f = e ∧ s(x, y) = s(u, v)

@[simp]

theorem Graph.singleEdge_inc_iff {α : Type u_1} {β : Type u_2} {x u v : α} {e f : β} : (Graph.singleEdge u v e).Inc f x ↔ f = e ∧ (x = u ∨ x = v)

@[simp]

theorem Graph.singleEdge_adj_iff {α : Type u_1} {β : Type u_2} {x y u v : α} {e : β} : (Graph.singleEdge u v e).Adj x y ↔ x = u ∧ y = v ∨ x = v ∧ y = u

@[simp]

theorem Graph.singleEdge_le_iff {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} : Graph.singleEdge u v e ≤ G ↔ G.IsLink e u v

@[simp]

theorem Graph.bouquet_incEdges {α : Type u_1} {β : Type u_2} {v : α} {F : Set β} : E(bouquet v F, v) = F

@[simp]

theorem Graph.bouquet_le_iff_of_mem {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} (hv : v ∈ G.vertexSet) (F : Set β) : bouquet v F ≤ G ↔ ∀ e ∈ F, G.IsLoopAt e v

@[simp]

theorem Graph.bouquet_le_iff_of_nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (v : α) (hF : F.Nonempty) : bouquet v F ≤ G ↔ ∀ e ∈ F, G.IsLoopAt e v

@[simp]

theorem Graph.banana_singleton {α : Type u_1} {β : Type u_2} {a b : α} (e : β) : banana a b {e} = Graph.singleEdge a b e

@[simp]

theorem Graph.restrict_banana {α : Type u_1} {β : Type u_2} (a b : α) (F R : Set β) : (banana a b F).restrict R = banana a b (F ∩ R)

@[simp]

theorem Graph.restrict_bouquet {α : Type u_1} {β : Type u_2} (v : α) (F R : Set β) : (bouquet v F).restrict R = bouquet v (F ∩ R)

@[simp]

theorem Graph.deleteEdges_banana {α : Type u_1} {β : Type u_2} (a b : α) (F R : Set β) : (banana a b F).deleteEdges R = banana a b (F \ R)

@[simp]

theorem Graph.deleteEdges_bouquet {α : Type u_1} {β : Type u_2} (v : α) (F R : Set β) : (bouquet v F).deleteEdges R = bouquet v (F \ R)

@[deprecated Graph.IsSpanningSubgraph.banana_mono (since := "2026-05-04")]

theorem Graph.banana_mono {α : Type u_1} {β : Type u_2} {a b : α} {X Y : Set β} (hXY : X ⊆ Y) : banana a b X ≤s banana a b Y

@[simp]

theorem Graph.banana_incEdges_left {α : Type u_1} {β : Type u_2} {a b : α} {F : Set β} : E(banana a b F, a) = F

@[simp]

theorem Graph.banana_incEdges_right {α : Type u_1} {β : Type u_2} {a b : α} {F : Set β} : E(banana a b F, b) = F

Complete graphs

def Graph.CompleteGraph (n : ℕ) : Graph ℕ (Sym2 ℕ)

The complete graph on n vertices.

Equations

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

@[simp]

theorem Graph.CompleteGraph_isLink (n : ℕ) (e : Sym2 ℕ) (x y : ℕ) : (CompleteGraph n).IsLink e x y = (x < n ∧ y < n ∧ x ≠ y ∧ e = s(x, y))

@[simp]

theorem Graph.edgeSet_CompleteGraph (n : ℕ) : (CompleteGraph n).edgeSet = {s : Sym2 ℕ | (∀ i ∈ s, i < n) ∧ ¬s.IsDiag}

@[simp]

theorem Graph.vertexSet_CompleteGraph (n : ℕ) : (CompleteGraph n).vertexSet = Set.Iio n

@[simp]

theorem Graph.inc_completeGraph (n x : ℕ) (e : Sym2 ℕ) : (CompleteGraph n).Inc e x ↔ x ∈ e ∧ e ∈ (CompleteGraph n).edgeSet

@[simp]

theorem Graph.completeGraph_adj (n x y : ℕ) (hx : x < n) (hy : y < n) : (CompleteGraph n).Adj x y ↔ x ≠ y

@[simp]

theorem Graph.encard_vertexSet_completeGraph (n : ℕ) : (CompleteGraph n).vertexSet.encard = ↑n

@[simp]

theorem Graph.encard_edgeSet_completeGraph (n : ℕ) : (CompleteGraph n).edgeSet.encard = ↑(n.choose 2)

@[simp]

theorem Graph.neighbors_completeGraph (n x : ℕ) (hx : x < n) : N(CompleteGraph n, x) = Set.Iio n \ {x}

@[simp]

theorem Graph.encard_neighbors_completeGraph (n x : ℕ) (hx : x < n) : N(CompleteGraph n, x).encard = ↑n - 1

@[simp]

theorem Graph.incEdges_completeGraph (n x : ℕ) (hx : x < n) : E(CompleteGraph n, x) = {x_1 : Sym2 ℕ | ∃ y ∈ Set.Iio n \ {x}, s(x, y) = x_1}

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

Equations

• G.IsComplete = ∀ x ∈ G.vertexSet, ∀ y ∈ G.vertexSet, x ≠ y → G.Adj x y

@[simp]

theorem Graph.completeGraph_isComplete (n : ℕ) : (CompleteGraph n).IsComplete

@[simp]

theorem Graph.bot_isComplete {α : Type u_1} {β : Type u_2} : ⊥.IsComplete

@[simp]

theorem Graph.bouquet_isComplete {α : Type u_1} {β : Type u_2} (v : α) (F : Set β) : (bouquet v F).IsComplete

@[simp]

theorem Graph.singleEdge_isComplete {α : Type u_1} {β : Type u_2} (u v : α) (e : β) : (Graph.singleEdge u v e).IsComplete

theorem Graph.banana_isComplete {α : Type u_1} {β : Type u_2} {F : Set β} (a b : α) (hF : F.Nonempty) : (banana a b F).IsComplete

@[simp]

theorem Graph.banana_isComplete_iff {α : Type u_1} {β : Type u_2} (a b : α) (F : Set β) : (banana a b F).IsComplete ↔ a = b ∨ F.Nonempty

def Graph.CompleteBipartiteGraph (m n : ℕ) : Graph (ℕ ⊕ ℕ) (ℕ × ℕ)

The complete bipartite graph with left part {0, ..., m - 1} and right part {0, ..., n - 1}.

Equations

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

@[simp]

theorem Graph.vertexSet_CompleteBipartiteGraph (m n : ℕ) : (CompleteBipartiteGraph m n).vertexSet = {x : ℕ ⊕ ℕ | match x with | Sum.inl i => i < m | Sum.inr j => j < n}

@[simp]

theorem Graph.CompleteBipartiteGraph_isLink (m n : ℕ) (e : ℕ × ℕ) (x y : ℕ ⊕ ℕ) : (CompleteBipartiteGraph m n).IsLink e x y = (e.1 < m ∧ e.2 < n ∧ (x = Sum.inl e.1 ∧ y = Sum.inr e.2 ∨ x = Sum.inr e.2 ∧ y = Sum.inl e.1))

@[simp]

theorem Graph.edgeSet_CompleteBipartiteGraph (m n : ℕ) : (CompleteBipartiteGraph m n).edgeSet = {e : ℕ × ℕ | e.1 < m ∧ e.2 < n}

@[simp]

theorem Graph.completeBipartiteGraph_adj_iff (m n : ℕ) (x y : ℕ ⊕ ℕ) : (CompleteBipartiteGraph m n).Adj x y ↔ (∃ i < m, ∃ j < n, x = Sum.inl i ∧ y = Sum.inr j) ∨ ∃ i < m, ∃ j < n, x = Sum.inr j ∧ y = Sum.inl i

@[simp]

theorem Graph.encard_vertexSet_completeBipartiteGraph (m n : ℕ) : (CompleteBipartiteGraph m n).vertexSet.encard = ↑m + ↑n

@[simp]

theorem Graph.encard_edgeSet_completeBipartiteGraph (m n : ℕ) : (CompleteBipartiteGraph m n).edgeSet.encard = ↑m * ↑n

def Graph.StarGraph {α : Type u_1} {β : Type u_2} (v : α) (f : β →. α) : Graph α β

The star graph with n leaves with center v

Equations

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

@[simp]

theorem Graph.edgeSet_StarGraph {α : Type u_1} {β : Type u_2} (v : α) (f : β →. α) : (StarGraph v f).edgeSet = f.Dom

@[simp]

theorem Graph.vertexSet_StarGraph {α : Type u_1} {β : Type u_2} (v : α) (f : β →. α) : (StarGraph v f).vertexSet = {v} ∪ f.ran

@[simp]

theorem Graph.StarGraph_isLink {α : Type u_1} {β : Type u_2} (v : α) (f : β →. α) (e : β) (x y : α) : (StarGraph v f).IsLink e x y = ∃ (he : e ∈ f.Dom), s(v, f.fn e he) = s(x, y)

@[simp]

theorem Graph.starGraph_inc_iff {α : Type u_1} {β : Type u_2} (v : α) (f : β →. α) (e : β) (x : α) : (StarGraph v f).Inc e x ↔ v = x ∧ e ∈ f.Dom ∨ x ∈ f e

@[simp]

theorem Graph.starGraph_adj_iff {α : Type u_1} {β : Type u_2} (v : α) (f : β →. α) (x y : α) : (StarGraph v f).Adj x y ↔ v = x ∧ y ∈ f.ran ∨ v = y ∧ x ∈ f.ran

def Graph.fromList {α : Type u_1} (S : Set α) (l : List (α × α)) : Graph α ℕ

The graph with vertex set S and edges over ℕ between pairs of vertices according to the list l.

Equations

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

@[simp]

theorem Graph.fromList_isLink {α : Type u_1} (S : Set α) (l : List (α × α)) (e : ℕ) (x y : α) : (fromList S l).IsLink e x y = ∃ (p : α × α), l[e]? = some p ∧ s(x, y) = s(p.1, p.2)

@[simp]

theorem Graph.edgeSet_fromList {α : Type u_1} (S : Set α) (l : List (α × α)) : (fromList S l).edgeSet = ↑(Finset.range l.length)

@[simp]

theorem Graph.vertexSet_fromList {α : Type u_1} (S : Set α) (l : List (α × α)) : (fromList S l).vertexSet = S ∪ {x : α | ∃ p ∈ l, x = p.1 ∨ x = p.2}

def Graph.OfSimpleGraph {α : Type u_1} (G : SimpleGraph α) : Graph α (Sym2 α)

Equations

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

@[simp]

theorem Graph.vertexSet_OfSimpleGraph {α : Type u_1} (G : SimpleGraph α) : (OfSimpleGraph G).vertexSet = Set.univ

@[simp]

theorem Graph.OfSimpleGraph_isLink {α : Type u_1} (G : SimpleGraph α) (e : Sym2 α) (x y : α) : (OfSimpleGraph G).IsLink e x y = (G.Adj x y ∧ s(x, y) = e)

@[simp]

theorem Graph.edgeSet_OfSimpleGraph {α : Type u_1} (G : SimpleGraph α) : (OfSimpleGraph G).edgeSet = {s : Sym2 α | ∃ (x : α) (y : α), G.Adj x y ∧ s(x, y) = s}

def Graph.OfSimpleGraphSet {α : Type u_1} {S : Set α} (G : SimpleGraph ↑S) : Graph α (Sym2 α)

Equations

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

@[simp]

theorem Graph.edgeSet_OfSimpleGraphSet {α : Type u_1} {S : Set α} (G : SimpleGraph ↑S) : (OfSimpleGraphSet G).edgeSet = {s : Sym2 α | ∃ (x : ↑S) (y : ↑S), G.Adj x y ∧ s(↑x, ↑y) = s}

@[simp]

theorem Graph.OfSimpleGraphSet_isLink {α : Type u_1} {S : Set α} (G : SimpleGraph ↑S) (e : Sym2 α) (x y : α) : (OfSimpleGraphSet G).IsLink e x y = ∃ (hx : x ∈ S) (hy : y ∈ S), G.Adj ⟨x, hx⟩ ⟨y, hy⟩ ∧ s(x, y) = e

@[simp]

theorem Graph.vertexSet_OfSimpleGraphSet {α : Type u_1} {S : Set α} (G : SimpleGraph ↑S) : (OfSimpleGraphSet G).vertexSet = S

def Graph.LineSimpleGraph {α : Type u_1} {β : Type u_2} (G : Graph α β) : SimpleGraph ↑G.edgeSet

Equations

• G.LineSimpleGraph = SimpleGraph.fromRel fun (e f : ↑G.edgeSet) => ∃ (x : α), G.Inc (↑e) x ∧ G.Inc (↑f) x

@[simp]

theorem Graph.LineSimpleGraph_adj {α : Type u_1} {β : Type u_2} (G : Graph α β) (a b : ↑G.edgeSet) : G.LineSimpleGraph.Adj a b = (¬a = b ∧ ((∃ (x : α), G.Inc (↑a) x ∧ G.Inc (↑b) x) ∨ ∃ (x : α), G.Inc (↑b) x ∧ G.Inc (↑a) x))

def Graph.LineGraph {α : Type u_1} {β : Type u_2} (G : Graph α β) : Graph β (Sym2 β)

The line graph of a graph G is the simple graph with the same vertices as G and edges given by the pairs of edges in G that have a common vertex.

Equations

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

@[simp]

theorem Graph.vertexSet_LineGraph {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.LineGraph.vertexSet = G.edgeSet

@[simp]

theorem Graph.edgeSet_LineGraph {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.LineGraph.edgeSet = (fun (p : β × β) => s(p.1, p.2)) '' {x : β × β | ¬x.1 = x.2 ∧ ∃ (x_1 : α), G.Inc x.1 x_1 ∧ G.Inc x.2 x_1}

@[simp]

theorem Graph.LineGraph_isLink {α : Type u_1} {β : Type u_2} (G : Graph α β) (a : Sym2 β) (e f : β) : G.LineGraph.IsLink a e f = (s(e, f) = a ∧ ¬e = f ∧ ∃ (x : α), G.Inc e x ∧ G.Inc f x)

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

Equations

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

@[simp]

theorem Graph.lineGraph_inc {α : Type u_1} {β : Type u_2} (G : Graph α β) (s : Sym2 β) (e : β) : G.LineGraph.Inc s e ↔ s ∈ G.LineGraph.edgeSet ∧ e ∈ s

@[simp]

theorem Graph.lineGraph_adj {α : Type u_1} {β : Type u_2} (G : Graph α β) (e f : β) : G.LineGraph.Adj e f ↔ e ≠ f ∧ ∃ (x : α), G.Inc e x ∧ G.Inc f x

theorem Graph.lineGraph_bouquet_isComplete {α : Type u_1} {β : Type u_2} (v : α) (F : Set β) : (bouquet v F).LineGraph.IsComplete

theorem Graph.lineGraph_banana_isComplete {α : Type u_1} {β : Type u_2} (a b : α) (F : Set β) : (banana a b F).LineGraph.IsComplete

theorem Graph.lineGraph_singleEdge_isComplete {α : Type u_1} {β : Type u_2} (u v : α) (e : β) : (Graph.singleEdge u v e).LineGraph.IsComplete

theorem Graph.lineGraph_starGraph_isComplete {α : Type u_1} {β : Type u_2} (v : α) (f : β →. α) : (StarGraph v f).LineGraph.IsComplete

def Graph.mixedLineGraph {α : Type u_1} {β : Type u_2} (G : Graph α β) : Graph (α ⊕ β) (α × β)

Note: a loop becomes a leaf.

Equations

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

@[simp]

theorem Graph.mixedLineGraph_isLink {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : α × β) (x y : α ⊕ β) : G.mixedLineGraph.IsLink e x y = (G.Inc e.2 e.1 ∧ s(Sum.inl e.1, Sum.inr e.2) = s(x, y))

@[simp]

theorem Graph.edgeSet_mixedLineGraph {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.mixedLineGraph.edgeSet = {(a, b) : α × β | G.Inc b a}

@[simp]

theorem Graph.vertexSet_mixedLineGraph {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.mixedLineGraph.vertexSet = Sum.inl '' G.vertexSet ∪ Sum.inr '' G.edgeSet

def Graph.«termL'(_)» : Lean.ParserDescr

Equations

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

@[simp]

theorem Graph.mixedLineGraph_inc {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : α × β) (a : α ⊕ β) : G.mixedLineGraph.Inc e a ↔ G.Inc e.2 e.1 ∧ (Sum.inr e.2 = a ∨ Sum.inl e.1 = a)

theorem Graph.mixedLineGraph_adj {α : Type u_1} {β : Type u_2} (G : Graph α β) (a b : α ⊕ β) : G.mixedLineGraph.Adj a b ↔ ∃ (x : α) (e : β), G.Inc e x ∧ s(Sum.inl x, Sum.inr e) = s(a, b)

@[simp]

theorem Graph.mixedLineGraph_vertex_not_adj {α : Type u_1} {β : Type u_2} (G : Graph α β) (x y : α) : ¬G.mixedLineGraph.Adj (Sum.inl x) (Sum.inl y)

@[simp]

theorem Graph.mixedLineGraph_edge_not_adj {α : Type u_1} {β : Type u_2} (G : Graph α β) (e f : β) : ¬G.mixedLineGraph.Adj (Sum.inr e) (Sum.inr f)