def Graph.noEdge {α : Type u_1} (V : Set α) (β : Type u_3) : Graph α β

The graph with vertex set V and no edges

Equations

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

@[simp]

theorem Graph.noEdge_edgeSet {α : Type u_1} (V : Set α) (β : Type u_3) : (Graph.noEdge V β).edgeSet = ∅

@[simp]

theorem Graph.noEdge_vertexSet {α : Type u_1} (V : Set α) (β : Type u_3) : (Graph.noEdge V β).vertexSet = V

@[simp]

theorem Graph.noEdge_isLink {α : Type u_1} (V : Set α) (β : Type u_3) (x✝ : β) (x✝¹ x✝² : α) : (Graph.noEdge V β).IsLink x✝ x✝¹ x✝² = False

@[simp]

theorem Graph.noEdge_le_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {V : Set α} : Graph.noEdge V β ≤ G ↔ V ⊆ G.vertexSet

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem Graph.le_noEdge_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} : G ≤ Graph.noEdge X β ↔ G.vertexSet ⊆ X ∧ G.edgeSet = ∅

instance Graph.instOrderBot_matroid {α : Type u_1} {β : Type u_2} : OrderBot (Graph α β)

Equations

• Graph.instOrderBot_matroid = { bot := Graph.noEdge ∅ β, bot_le := ⋯ }

@[simp]

theorem Graph.bot_vertexSet {α : Type u_1} {β : Type u_2} : ⊥.vertexSet = ∅

@[simp]

theorem Graph.bot_edgeSet {α : Type u_1} {β : Type u_2} : ⊥.vertexSet = ∅

@[simp]

theorem Graph.bot_isClosedSubgraph {α : Type u_1} {β : Type u_2} (G : Graph α β) : ⊥.IsClosedSubgraph G

@[simp]

theorem Graph.bot_isInducedSubgraph {α : Type u_1} {β : Type u_2} (G : Graph α β) : ⊥.IsInducedSubgraph G

@[simp]

theorem Graph.noEdge_empty {α : Type u_1} {β : Type u_2} : Graph.noEdge ∅ β = ⊥

@[simp]

theorem Graph.bot_not_isLink {α : Type u_1} {β : Type u_2} {x y : α} {e : β} : ¬⊥.IsLink e x y

theorem Graph.eq_bot_or_vertexSet_nonempty {α : Type u_1} {β : Type u_2} (G : Graph α β) : G = ⊥ ∨ G.vertexSet.Nonempty

@[simp]

theorem Graph.vertexSet_eq_empty_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.vertexSet = ∅ ↔ G = ⊥

@[simp]

theorem Graph.vertexSet_nonempty_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.vertexSet.Nonempty ↔ G ≠ ⊥

theorem Graph.ne_bot_of_mem_vertexSet {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (h : x ∈ G.vertexSet) : G ≠ ⊥

instance Graph.instInhabited_matroid {α : Type u_1} {β : Type u_2} : Inhabited (Graph α β)

Equations

• Graph.instInhabited_matroid = { default := ⊥ }

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.singleEdge_edgeSet {α : 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))

@[simp]

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

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

Graphs with one vertex

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

A graph with one vertex and loops at that vertex

Equations

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

@[simp]

theorem Graph.bouquet_isLink {α : Type u_1} {β : Type u_2} (v : α) (F : Set β) (e : β) (x y : α) : (bouquet v F).IsLink e x y = (e ∈ F ∧ x = v ∧ y = v)

@[simp]

theorem Graph.bouquet_edgeSet {α : Type u_1} {β : Type u_2} (v : α) (F : Set β) : (bouquet v F).edgeSet = F

@[simp]

theorem Graph.bouquet_vertexSet {α : Type u_1} {β : Type u_2} (v : α) (F : Set β) : (bouquet v F).vertexSet = {v}

@[simp]

theorem Graph.bouquet_inc_iff {α : Type u_1} {β : Type u_2} {x v : α} {e : β} {F : Set β} : (bouquet v F).Inc e x ↔ e ∈ F ∧ x = v

@[simp]

theorem Graph.bouquet_isLoopAt {α : Type u_1} {β : Type u_2} {x v : α} {e : β} {F : Set β} : (bouquet v F).IsLoopAt e x ↔ e ∈ F ∧ x = v

@[simp]

theorem Graph.bouquet_not_isNonloopAt {α : Type u_1} {β : Type u_2} {x v : α} {e : β} {F : Set β} : ¬(bouquet v F).IsNonloopAt e x

theorem Graph.eq_bouquet {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} (hv : v ∈ G.vertexSet) (hss : G.vertexSet.Subsingleton) : G = bouquet v G.edgeSet

Every graph on just one vertex is a bouquet on that vertex

theorem Graph.exists_eq_bouquet_edge {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} (hv : v ∈ G.vertexSet) (hss : G.vertexSet.Subsingleton) : ∃ (F : Set β), G = bouquet v F

Every graph on just one vertex is a bouquet on that vertex

theorem Graph.exists_eq_bouquet {α : Type u_1} {β : Type u_2} {G : Graph α β} (hne : G.vertexSet.Nonempty) (hss : G.vertexSet.Subsingleton) : ∃ (x : α) (F : Set β), G = bouquet x F

theorem Graph.bouquet_empty {α : Type u_1} {β : Type u_2} (v : α) : bouquet v ∅ = Graph.noEdge {v} β

theorem Graph.bouquet_mono {α : Type u_1} {β : Type u_2} (v : α) {X Y : Set β} (hss : X ⊆ Y) : bouquet v X ≤s bouquet v Y

Two vertices

def Graph.banana {α : Type u_1} {β : Type u_2} (a b : α) (F : Set β) : Graph α β

A graph with exactly two vertices and no loops.

Equations

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

@[simp]

theorem Graph.banana_isLink {α : Type u_1} {β : Type u_2} (a b : α) (F : Set β) (e : β) (x y : α) : (banana a b F).IsLink e x y = (e ∈ F ∧ (x = a ∧ y = b ∨ x = b ∧ y = a))

@[simp]

theorem Graph.banana_edgeSet {α : Type u_1} {β : Type u_2} (a b : α) (F : Set β) : (banana a b F).edgeSet = F

@[simp]

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

@[simp]

theorem Graph.banana_inc_iff {α : Type u_1} {β : Type u_2} {x a b : α} {e : β} {F : Set β} : (banana a b F).Inc e x ↔ e ∈ F ∧ (x = a ∨ x = b)

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

@[simp]

theorem Graph.banana_isNonloopAt_iff {α : Type u_1} {β : Type u_2} {x a b : α} {e : β} {F : Set β} : (banana a b F).IsNonloopAt e x ↔ e ∈ F ∧ (x = a ∨ x = b) ∧ a ≠ b

@[simp]

theorem Graph.banana_isLoopAt_iff {α : Type u_1} {β : Type u_2} {x a b : α} {e : β} {F : Set β} : (banana a b F).IsLoopAt e x ↔ e ∈ F ∧ x = a ∧ a = b

@[simp]

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

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

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_edgeSet (n : ℕ) : (CompleteGraph n).edgeSet = {s : Sym2 ℕ | (∀ i ∈ s, i < n) ∧ ¬s.IsDiag}

@[simp]

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

@[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.CompleteGraph_adj (n x y : ℕ) (hx : x < n) (hy : y < n) : (CompleteGraph n).Adj x y ↔ x ≠ y

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

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

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.StarGraph_vertexSet {α : Type u_1} {β : Type u_2} (v : α) (f : β →. α) : (StarGraph v f).vertexSet = {v} ∪ f.ran

@[simp]

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

@[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)

Graph constructor from a list of pairs of vertices

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_vertexSet {α : Type u_1} (S : Set α) (l : List (α × α)) : (fromList S l).vertexSet = S ∪ {x : α | ∃ p ∈ l, x = p.1 ∨ x = p.2}

@[simp]

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

@[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)