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

G.DegreePos means that G has no degree-zero vertices.

Equations

• G.DegreePos = ∀ ⦃x : α⦄, x ∈ G.vertexSet → ∃ (e : β), G.Inc e x

theorem Graph.DegreePos.one_le_eDegree {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (hG : G.DegreePos) (hx : x ∈ G.vertexSet) : 1 ≤ G.eDegree x

theorem Graph.DegreePos.one_le_degree {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.LocallyFinite] (hG : G.DegreePos) (hx : x ∈ G.vertexSet) : 1 ≤ G.degree x

theorem Graph.degreePos_iff' {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.DegreePos ↔ ∀ ⦃x : α⦄, x ∈ G.vertexSet → G.eDegree x ≠ 0

theorem Graph.degreePos_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.LocallyFinite] : G.DegreePos ↔ ∀ ⦃x : α⦄, x ∈ G.vertexSet → G.degree x ≠ 0

theorem Graph.DegreePos.finite_of_edgeSet_finite {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.DegreePos) (hE : G.edgeSet.Finite) : G.Finite

theorem Graph.DegreePos.edgeSet_finite_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.DegreePos) : G.edgeSet.Finite ↔ G.Finite

theorem Graph.DegreePos.edgeSet_nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.DegreePos) (hV : G.vertexSet.Nonempty) : G.edgeSet.Nonempty

def Graph.MaxDegreeLE {α : Type u_1} {β : Type u_2} (G : Graph α β) (d : ℕ) : Prop

G.MaxDegreeLE d means that G has maximum degree at most d.

Equations

• G.MaxDegreeLE d = ∀ (v : α), G.eDegree v ≤ ↑d

theorem Graph.MaxDegreeLE.degree_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} (h : G.MaxDegreeLE d) (v : α) : G.degree v ≤ d

theorem Graph.MaxDegreeLE.mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} {d : ℕ} (h : G.MaxDegreeLE d) (hle : H ≤ G) : H.MaxDegreeLE d

theorem Graph.MaxDegreeLE.locallyFinite {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} (h : G.MaxDegreeLE d) : G.LocallyFinite

theorem Graph.maxDegreeLE_iff' {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} : G.MaxDegreeLE d ↔ ∀ v ∈ G.vertexSet, G.eDegree v ≤ ↑d

A version of maxDegreeLE_iff for infinite graphs.

theorem Graph.maxDegreeLE_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} [G.LocallyFinite] : G.MaxDegreeLE d ↔ ∀ v ∈ G.vertexSet, G.degree v ≤ d

theorem Graph.MaxDegreeLE.encard_edgeSet_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} (h : G.MaxDegreeLE d) : 2 * G.edgeSet.encard ≤ ↑d * G.vertexSet.encard

theorem Graph.MaxDegreeLE.ncard_edgeSet_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} [G.Finite] (h : G.MaxDegreeLE d) : 2 * G.edgeSet.ncard ≤ d * G.vertexSet.ncard

theorem Graph.MaxDegreeLE.finite_of_vertexSet_finite {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} (h : G.MaxDegreeLE d) (hV : G.vertexSet.Finite) : G.Finite

theorem Graph.maxDegreeLE_zero_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.MaxDegreeLE 0 ↔ G = noEdge G.vertexSet β

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

Equations

• G.minEDegree = ⨅ x ∈ G.vertexSet, G.eDegree x

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

Equations

• G.minDegree = G.minEDegree.toNat

theorem Graph.natCast_minDegree_eq {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.LocallyFinite] (hG : G.vertexSet.Nonempty) : ↑G.minDegree = G.minEDegree

@[simp]

theorem Graph.minEDegree_bot {α : Type u_1} {β : Type u_2} : ⊥.minEDegree = ⊤

theorem Graph.minEDegree_eq_top {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.minEDegree = ⊤) : G = ⊥ ∨ ¬G.LocallyFinite

@[simp]

theorem Graph.minDegree_bot {α : Type u_1} {β : Type u_2} : ⊥.minDegree = 0

theorem Graph.minEDegree_le_eDegree {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (hx : x ∈ G.vertexSet) : G.minEDegree ≤ G.eDegree x

theorem Graph.minDegree_le_degree {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.LocallyFinite] (hx : x ∈ G.vertexSet) : G.minDegree ≤ G.degree x

theorem Graph.ENat.exists_eq_biInf {ι : Type u_3} {S : Set ι} (hS : S.Nonempty) (f : ι → ℕ∞) : ∃ a ∈ S, f a = ⨅ x ∈ S, f x

theorem Graph.exists_vertex_minEDegree {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.vertexSet.Nonempty) : ∃ x ∈ G.vertexSet, G.eDegree x = G.minEDegree

theorem Graph.exists_vertex_minDegree {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.vertexSet.Nonempty) : ∃ x ∈ G.vertexSet, G.degree x = G.minDegree

theorem Graph.encard_neighbors_le {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.Simple] (h : x ∈ G.vertexSet) : N(G, x).encard + 1 ≤ G.vertexSet.encard

theorem Graph.eDegree_le_encard {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.Simple] (h : x ∈ G.vertexSet) : G.eDegree x + 1 ≤ G.vertexSet.encard

theorem Graph.degree_le_ncard {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.Simple] [G.Finite] (h : x ∈ G.vertexSet) : G.degree x + 1 ≤ G.vertexSet.ncard

theorem Graph.degree_lt_ncard {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.Simple] [G.Finite] (h : x ∈ G.vertexSet) : G.degree x < G.vertexSet.ncard

theorem Graph.minEDegree_le_encard {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Simple] (hne : G.vertexSet.Nonempty) : G.minEDegree + 1 ≤ G.vertexSet.encard

theorem Graph.minDegree_lt_ncard {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Simple] [G.Finite] (hNe : G.vertexSet.Nonempty) : G.minDegree < G.vertexSet.ncard

theorem Graph.unique_neighbor_of_eDegree_eq_one {α : Type u_1} {β : Type u_2} {x y z : α} {G : Graph α β} (hx : G.eDegree x = 1) (hxy : G.Adj x y) (hxz : G.Adj x z) : y = z

theorem Graph.IsSpanningSubgraph.minEDegree {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H ≤s G) : H.minEDegree ≤ G.minEDegree

def Graph.MinDegreeGE {α : Type u_1} {β : Type u_2} (G : Graph α β) (d : ℕ) : Prop

G.MinDegreeGE d means that G has minimum degree at least d.

Equations

• G.MinDegreeGE d = ∀ v ∈ G.vertexSet, ↑d ≤ G.eDegree v

theorem Graph.MinDegreeGE.le_degree {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} [G.LocallyFinite] (h : G.MinDegreeGE d) (v : α) (hv : v ∈ G.vertexSet) : d ≤ G.degree v

theorem Graph.MinDegreeGE.mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} {d : ℕ} (h : G.MinDegreeGE d) (hle : G ≤ H) (hV : H.vertexSet ⊆ G.vertexSet) : H.MinDegreeGE d

theorem Graph.minDegreeGE_iff' {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} : G.MinDegreeGE d ↔ ∀ v ∈ G.vertexSet, ↑d ≤ G.eDegree v

theorem Graph.minDegreeGE_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} [G.LocallyFinite] : G.MinDegreeGE d ↔ ∀ v ∈ G.vertexSet, d ≤ G.degree v

theorem Graph.MinDegreeGE.le_encard_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} (h : G.MinDegreeGE d) : ↑d * G.vertexSet.encard ≤ 2 * G.edgeSet.encard

theorem Graph.MinDegreeGE.le_ncard_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} [G.Finite] (h : G.MinDegreeGE d) : d * G.vertexSet.ncard ≤ 2 * G.edgeSet.ncard

def Graph.Regular {α : Type u_1} {β : Type u_2} (G : Graph α β) (d : ℕ) : Prop

G.Regular d means that every vertex has degree d.

Equations

• G.Regular d = ∀ ⦃v : α⦄, v ∈ G.vertexSet → G.eDegree v = ↑d

theorem Graph.Regular.degree {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} {d : ℕ} (hG : G.Regular d) (hv : v ∈ G.vertexSet) : G.degree v = d

theorem Graph.regular_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} [G.LocallyFinite] : G.Regular d ↔ ∀ v ∈ G.vertexSet, G.degree v = d

theorem Graph.Regular.maxDegreeLE {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} (hG : G.Regular d) : G.MaxDegreeLE d

theorem Graph.Regular.encard_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} (hG : G.Regular d) : 2 * G.edgeSet.encard = ↑d * G.vertexSet.encard

theorem Graph.Regular.degreePos {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} (hG : G.Regular d) (hd : d ≠ 0) : G.DegreePos

theorem Graph.Regular.edgeSet_finite_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} (hG : G.Regular d) (hd : d ≠ 0) : G.edgeSet.Finite ↔ G.Finite

theorem Graph.Regular.ncard_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} (hG : G.Regular d) : 2 * G.edgeSet.ncard = d * G.vertexSet.ncard

theorem Graph.Regular.of_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {d : ℕ} (hG : G.Regular d) (hH : H.IsClosedSubgraph G) : H.Regular d