theorem List.eq_of_sum_eq_le {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] [AddLeftMono α] {l : List (α × α)} (hle : ∀ x ∈ l, x.1 ≤ x.2) (hsum : l.unzip.1.sum = l.unzip.2.sum) : l.unzip.1 = l.unzip.2

theorem Graph.disjoint_isLoopAt_isNonLoopAt {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} : Disjoint {e : β | G.IsLoopAt e x} {e : β | G.IsNonloopAt e x}

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

@[simp]

theorem Graph.subsingleton_setOf_isLink {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (x : α) : {y : α | G.IsLink e x y}.Subsingleton

@[simp]

theorem Graph.endSet_finite {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) : V(G, e).Finite

noncomputable def Graph.incFun {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) : α →₀ ℕ

The 'incidence function' of a graph G. If e : β and x : α, then G.incFun e x is equal to 0 if e is not incident to x, 1 if e is a nonloop edge at x and 2 if e is a loop edge at x. It is defined this way so that G.incFun e sums to two for each e ∈ E(G), which is natural for the handshake theorem and linear algebra on graphs.

The definition is contrivedly written in terms of ncard so it does not require any explicit decidability assumptions.

Equations

• G.incFun e = { support := ⋯.toFinset, toFun := fun (x : α) => {y : α | G.IsLink e x y}.ncard + ({y : α | G.IsLink e x y} ∩ {x}).ncard, mem_support_toFun := ⋯ }

theorem Graph.IsLink.incFun_support_eq {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} [DecidableEq α] (h : G.IsLink e x y) : (G.incFun e).support = {x, y}

@[simp]

theorem Set.singleton_inter_eq {α : Type u_1} (x : α) (s : Set α) [Decidable (x ∈ s)] : {x} ∩ s = if x ∈ s then {x} else ∅

@[simp]

theorem Set.inter_singleton_eq {α : Type u_1} (x : α) (s : Set α) [Decidable (x ∈ s)] : s ∩ {x} = if x ∈ s then {x} else ∅

theorem Graph.incFun_eq_zero_of_notMem {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} (he : e ∉ G.edgeSet) : G.incFun e = 0

theorem Graph.incFun_le_two {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (x : α) : (G.incFun e) x ≤ 2

theorem Graph.IsNonloopAt.eIncFun_eq_one {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsNonloopAt e x) : (G.incFun e) x = 1

@[simp]

theorem Graph.incFun_eq_one_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} : (G.incFun e) x = 1 ↔ G.IsNonloopAt e x

theorem Graph.IsNonloopAt.incFun_eq_one {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsNonloopAt e x) : (G.incFun e) x = 1

@[simp]

theorem Graph.incFun_eq_two_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} : (G.incFun e) x = 2 ↔ G.IsLoopAt e x

theorem Graph.IsLoopAt.incFun_eq_two {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} : G.IsLoopAt e x → (G.incFun e) x = 2

Alias of the reverse direction of Graph.incFun_eq_two_iff.

theorem Graph.Inc.incFun_ne_zero {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) : (G.incFun e) x ≠ 0

theorem Graph.Inc.one_le_incFun {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) : 1 ≤ (G.incFun e) x

@[simp]

theorem Graph.incFun_eq_zero_iff {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} : G.incFun e = 0 ↔ e ∉ G.edgeSet

theorem Graph.sum_incFun_eq_two {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} (he : e ∈ G.edgeSet) : ((G.incFun e).sum fun (x : α) (x_1 : ℕ) => x_1) = 2

@[simp]

theorem Graph.incFun_vertex_eq_zero_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} : (G.incFun e) x = 0 ↔ ¬G.Inc e x

theorem Graph.map_incFun {α : Type u_1} {β : Type u_2} {x : α} (G : Graph α β) {α' : Type u_3} {φ : α → α'} (hf : Set.InjOn φ G.vertexSet) (e : β) (hx : x ∈ G.vertexSet) : ((map φ G).incFun e) (φ x) = (G.incFun e) x

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

theorem Graph.edgeMap_incFun_of_injective {α : Type u_1} {β : Type u_2} (G : Graph α β) {β' : Type u_3} {φ : β → β'} (hφ : Function.Injective φ) {e : β} : (G.edgeMap φ ⋯).incFun (φ e) = G.incFun e

theorem Graph.map_incFun_of_injective {α : Type u_1} {β : Type u_2} {x : α} (G : Graph α β) {α' : Type u_3} {φ : α → α'} (hφ : Function.Injective φ) (e : β) : ((map φ G).incFun e) (φ x) = (G.incFun e) x

Vertex Degrees

noncomputable def Graph.eDegree {α : Type u_1} {β : Type u_2} (G : Graph α β) (v : α) : ℕ∞

The degree of a vertex as a term in ℕ∞.

Equations

• G.eDegree v = ∑' (e : β), ↑((G.incFun e) v)

noncomputable def Graph.degree {α : Type u_1} {β : Type u_2} (G : Graph α β) (v : α) : ℕ

The degree of a vertex as a term in ℕ (with value zero if the degree is infinite).

Equations

• G.degree v = (G.eDegree v).toNat

theorem Graph.eDegree_eq_tsum_mem {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} : G.eDegree x = ∑' (e : ↑E(G, x)), ↑((G.incFun ↑e) x)

theorem Graph.eDegree_le_two_mul_encard_setOf_inc {α : Type u_1} {β : Type u_2} (G : Graph α β) (v : α) : G.eDegree v ≤ 2 * E(G, v).encard

theorem Graph.eDegree_le_two_mul_card_edgeSet {α : Type u_1} {β : Type u_2} (G : Graph α β) (v : α) : G.eDegree v ≤ 2 * G.edgeSet.encard

@[simp]

theorem Graph.natCast_degree_eq {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.LocallyFinite] (v : α) : ↑(G.degree v) = G.eDegree v

theorem Graph.eDegree_map {α : Type u_1} {β : Type u_2} (G : Graph α β) (v : α) {α' : Type u_3} {φ : α → α'} (h : Set.InjOn φ G.vertexSet) (hv : v ∈ G.vertexSet) : (map φ G).eDegree (φ v) = G.eDegree v

theorem Graph.eDegree_map_of_injective {α : Type u_1} {β : Type u_2} (G : Graph α β) (v : α) {α' : Type u_3} {φ : α → α'} (h : Function.Injective φ) : (map φ G).eDegree (φ v) = G.eDegree v

theorem Graph.eDegree_edgeMap {α : Type u_1} {β : Type u_2} (G : Graph α β) (v : α) {β' : Type u_3} {φ : β → β'} (hφ : Set.InjOn φ G.edgeSet) : (G.edgeMap φ ⋯).eDegree v = G.eDegree v

@[simp]

theorem Graph.eDegree_lt_top {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.LocallyFinite] : G.eDegree x < ⊤

@[simp]

theorem Graph.eDegree_ne_top {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.LocallyFinite] : G.eDegree x ≠ ⊤

@[simp]

theorem Graph.eDegree_eq_top {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (hx : G.eDegree x = ⊤) : ¬G.LocallyFinite

theorem Graph.eDegree_eq_zero_iff_inc {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} : G.eDegree v = 0 ↔ ∀ (e : β), ¬G.Inc e v

theorem Graph.eDegree_eq_zero_iff_adj {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} : G.eDegree v = 0 ↔ ∀ (x : α), ¬G.Adj v x

theorem Graph.degree_eq_zero_iff_inc {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} [G.LocallyFinite] : G.degree v = 0 ↔ ∀ (e : β), ¬G.Inc e v

theorem Graph.degree_ne_zero_iff_inc {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} [G.LocallyFinite] : G.degree v ≠ 0 ↔ ∃ (e : β), G.Inc e v

theorem Graph.degree_eq_zero_iff_adj {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} [G.LocallyFinite] : G.degree v = 0 ↔ ∀ (x : α), ¬G.Adj v x

theorem Graph.degree_ne_zero_iff_adj {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} [G.LocallyFinite] : G.degree v ≠ 0 ↔ ∃ (x : α), G.Adj v x

theorem Graph.eDegree_eq_zero_of_notMem {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} (hv : v ∉ G.vertexSet) : G.eDegree v = 0

theorem Graph.degree_eq_zero_of_notMem {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} (hv : v ∉ G.vertexSet) : G.degree v = 0

theorem Graph.degree_eq_fintype_sum {α : Type u_1} {β : Type u_2} [Fintype β] (G : Graph α β) (v : α) : G.degree v = ∑ e : β, (G.incFun e) v

theorem Graph.degree_eq_finsum {α : Type u_1} {β : Type u_2} (G : Graph α β) (v : α) : G.degree v = ∑ᶠ (e : β), (G.incFun e) v

@[simp]

theorem Graph.finsum_incFun_eq {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} (he : e ∈ G.edgeSet) : ∑ᶠ (v : α), (G.incFun e) v = 2

@[simp]

theorem Graph.tsum_incFun_eq {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} (he : e ∈ G.edgeSet) : ∑' (v : α), ↑((G.incFun e) v) = 2

theorem Graph.IsLoopAt.two_le_eDegree {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e x) : 2 ≤ G.eDegree x

theorem Graph.IsNonloopAt.one_le_eDegree {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsNonloopAt e x) : 1 ≤ G.eDegree x

theorem Graph.Inc.one_le_eDegree {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) : 1 ≤ G.eDegree x

theorem Graph.IsLoopAt.two_le_degree {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} [G.LocallyFinite] (h : G.IsLoopAt e x) : 2 ≤ G.degree x

theorem Graph.Inc.one_le_degree {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} [G.LocallyFinite] (h : G.Inc e x) : 1 ≤ G.degree x

theorem Graph.IsNonloopAt.one_le_degree {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} [G.LocallyFinite] (h : G.IsNonloopAt e x) : 1 ≤ G.degree x

@[simp]

theorem Graph.support_degree_subset {α : Type u_1} {β : Type u_2} (G : Graph α β) : Function.support G.degree ⊆ G.vertexSet

@[simp]

theorem Graph.support_eDegree_subset {α : Type u_1} {β : Type u_2} (G : Graph α β) : Function.support G.eDegree ⊆ G.vertexSet

theorem Graph.handshake_eDegree {α : Type u_1} {β : Type u_2} (G : Graph α β) : ∑' (v : α), G.eDegree v = 2 * G.edgeSet.encard

theorem Graph.handshake_eDegree_subtype {α : Type u_1} {β : Type u_2} (G : Graph α β) : ∑' (v : ↑G.vertexSet), G.eDegree ↑v = 2 * G.edgeSet.encard

theorem Graph.handshake_degree_subtype {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Finite] : ∑ᶠ (v : α) (_ : v ∈ G.vertexSet), G.degree v = 2 * G.edgeSet.ncard

theorem Graph.handshake_degree_finset {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Finite] : ∑ v ∈ ⋯.toFinset, G.degree v = 2 * ⋯.toFinset.card

theorem Graph.handshake {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Finite] : ∑ᶠ (v : α), G.degree v = 2 * G.edgeSet.ncard

This should only need LocallyFinite

theorem Graph.eDegree_eq_encard_add_encard {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : G.eDegree x = 2 * {e : β | G.IsLoopAt e x}.encard + {e : β | G.IsNonloopAt e x}.encard

theorem Graph.encard_setOf_inc_le_eDegree {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : E(G, x).encard ≤ G.eDegree x

theorem Graph.degree_eq_ncard_add_ncard {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.LocallyFinite] (x : α) : G.degree x = 2 * {e : β | G.IsLoopAt e x}.ncard + {e : β | G.IsNonloopAt e x}.ncard

theorem Graph.incEdges_eq_isLoopAt_union_isNonloopAt {α : Type u_1} {β : Type u_2} {y : α} {G : Graph α β} : E(G, y) = {e : β | G.IsLoopAt e y} ∪ {e : β | G.IsNonloopAt e y}

theorem Graph.encard_adj_le_encard_inc {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} : N(G, x).encard ≤ E(G, x).encard

theorem Graph.encard_inc_le_eDegree {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} : E(G, x).encard ≤ G.eDegree x

theorem Graph.eDegree_eq_encard_inc {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.Loopless] : G.eDegree x = E(G, x).encard

theorem Graph.degree_eq_ncard_inc {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.Loopless] : G.degree x = E(G, x).ncard

theorem Graph.eDegree_eq_encard_adj {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.Simple] : G.eDegree x = N(G, x).encard

theorem Graph.degree_eq_ncard_adj {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.Simple] : G.degree x = N(G, x).ncard

theorem Graph.locallyFinite_of_eDegree_ne_top {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : ∀ (x : α), G.eDegree x ≠ ⊤) : G.LocallyFinite

theorem Graph.forall_eDegree_ne_top_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : (∀ (x : α), G.eDegree x ≠ ⊤) ↔ G.LocallyFinite

theorem Graph.exists_eDegree_eq_top_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : (∃ (x : α), G.eDegree x = ⊤) ↔ ¬G.LocallyFinite

@[simp]

theorem Graph.natCast_degree_eq_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (v : α) : ↑(G.degree v) = G.eDegree v ↔ E(G, v).Finite

Subgraphs

theorem Graph.incFun_eq_of_le {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} (hle : H ≤ G) (he : e ∈ H.edgeSet) : (H.incFun e) x = (G.incFun e) x

theorem Graph.incFun_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : H ≤ G) (e : β) (x : α) : (H.incFun e) x ≤ (G.incFun e) x

theorem Graph.eDegree_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : H ≤ G) (x : α) : H.eDegree x ≤ G.eDegree x

theorem Graph.degree_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} [hG : G.LocallyFinite] (hle : H ≤ G) (x : α) : H.degree x ≤ G.degree x

theorem Graph.IsClosedSubgraph.eDegree_eq {α : Type u_1} {β : Type u_2} {x : α} {G H : Graph α β} (h : H.IsClosedSubgraph G) (hx : x ∈ H.vertexSet) : H.eDegree x = G.eDegree x

theorem Graph.IsClosedSubgraph.degree_eq {α : Type u_1} {β : Type u_2} {x : α} {G H : Graph α β} (h : H.IsClosedSubgraph G) (hx : x ∈ H.vertexSet) : H.degree x = G.degree x

theorem Graph.incEdges_of_degree {α : Type u_1} {β : Type u_2} {x : α} {G H : Graph α β} [G.LocallyFinite] (hle : H ≤ G) (h : H.degree x = G.degree x) : E(H, x) = E(G, x)

Isolated vertices

theorem Graph.Isolated.eDegree {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (h : G.Isolated x) : G.eDegree x = 0

theorem Graph.isolated_iff_eDegree {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (hx : x ∈ G.vertexSet) : G.Isolated x ↔ G.eDegree x = 0

theorem Graph.Isolated.degree {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (h : G.Isolated x) : G.degree x = 0

theorem Graph.isolated_iff_degree {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.LocallyFinite] (hx : x ∈ G.vertexSet) : G.Isolated x ↔ G.degree x = 0

Leaves

theorem Graph.IsPendant.eDegree {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsPendant e x) : G.eDegree x = 1

theorem Graph.Inc.isPendant_of_eDegree_le_one {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) (hdeg : G.eDegree x ≤ 1) : G.IsPendant e x

theorem Graph.Inc.isPendant_of_degree_eq_one {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) (hdeg : G.degree x = 1) : G.IsPendant e x

theorem Graph.Inc.isPendant_of_degree_le_one {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} [G.LocallyFinite] (h : G.Inc e x) (hdeg : G.degree x ≤ 1) : G.IsPendant e x

theorem Graph.IsPendant.edgeSet_delete_vertex_eq {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsPendant e x) : (G.deleteVerts {x}).edgeSet = G.edgeSet \ {e}

theorem Graph.IsPendant.eq_addEdge {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsPendant e x) : ∃ y ∈ G.vertexSet, G.IsLink e x y ∧ y ≠ x ∧ e ∉ (G.deleteVerts {x}).edgeSet ∧ G = (G.deleteVerts {x}).addEdge e x y

theorem Graph.IsPendant.exists_eq_addEdge {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsPendant e x) : ∃ (y : α) (H : Graph α β), x ∉ H.vertexSet ∧ y ∈ H.vertexSet ∧ e ∉ H.edgeSet ∧ G = H.addEdge e x y

@[simp]

theorem Graph.eDegree_eq_one_iff {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} : G.eDegree v = 1 ↔ G.IsLeaf v

@[simp]

theorem Graph.degree_eq_one_iff {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} : G.degree v = 1 ↔ G.IsLeaf v

theorem Graph.IsLeaf.eDegree {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} (h : G.IsLeaf v) : G.eDegree v = 1

theorem Graph.IsLeaf.degree {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} (h : G.IsLeaf v) : G.degree v = 1