Incidence counts for multigraphs

This file counts actual multigraph edge identities incident to vertices and vertex sets. The two vertex counts differ only in their treatment of loops: Graph.incidenceCount counts a loop once, while Graph.nonloopIncidenceCount discards it. Parallel edges are always counted separately. Both definitions use Set.ncard, so they return zero when the set being counted is infinite.

For finite sets of actual vertices, Graph.neighborsIn G S T is the set of vertices in T joined by an edge to a vertex in S, ignoring edge multiplicity.

For finite actual edge sets, Graph.internalEdges and Graph.incidentEdges provide the finite sets of edges internal to, or incident with, a finite set of actual vertices. These are the counting objects used by degree arguments and by orientation constraints. The comparison with SimpleGraph.degree shows that the multigraph count specializes to the usual simple-graph degree. The edge-deletion results record that surviving incident edges together with deleted incident edges account for the original incidence count.

Neighbours within a set of vertices

noncomputable def Graph.neighborsIn {α : Type u} {β : Type v} (G : Graph α β) (S T : Finset ↑G.vertexSet) : Finset ↑G.vertexSet

The actual vertices of T joined by an edge to some vertex of S. A vertex joined to S by several parallel edges occurs once.

@[simp]

theorem Graph.mem_neighborsIn {α : Type u} {β : Type v} {G : Graph α β} {S T : Finset ↑G.vertexSet} {y : ↑G.vertexSet} : y ∈ G.neighborsIn S T ↔ y ∈ T ∧ ∃ x ∈ S, G.Adj ↑x ↑y

theorem Graph.neighborsIn_subset {α : Type u} {β : Type v} {G : Graph α β} {S T : Finset ↑G.vertexSet} : G.neighborsIn S T ⊆ T

theorem Graph.neighborsIn_mono {α : Type u} {β : Type v} {G : Graph α β} {S S' T : Finset ↑G.vertexSet} (hS : S ⊆ S') : G.neighborsIn S T ⊆ G.neighborsIn S' T

@[simp]

theorem Graph.neighborsIn_empty_left {α : Type u} {β : Type v} {G : Graph α β} {T : Finset ↑G.vertexSet} : G.neighborsIn ∅ T = ∅

@[simp]

theorem Graph.neighborsIn_empty_right {α : Type u} {β : Type v} {G : Graph α β} {S : Finset ↑G.vertexSet} : G.neighborsIn S ∅ = ∅

noncomputable def Graph.nonloopIncidenceCount {α : Type u} {β : Type v} (G : Graph α β) (x : α) : ℕ

The Set.ncard of the nonloop edge identities incident to a vertex of a multigraph. Parallel edges are counted separately; the result is zero when this set is infinite.

noncomputable def Graph.incidenceCount {α : Type u} {β : Type v} (G : Graph α β) (x : α) : ℕ

The Set.ncard of the edge identities incident to a vertex of a multigraph, counting each loop once and counting parallel edges separately. The result is zero when this set is infinite.

theorem Graph.nonloopIncidenceCount_def {α : Type u} {β : Type v} (G : Graph α β) (x : α) : G.nonloopIncidenceCount x = (incidenceSet x \ loopSet x).ncard

theorem Graph.incidenceCount_def {α : Type u} {β : Type v} (G : Graph α β) (x : α) : G.incidenceCount x = (incidenceSet x).ncard

theorem Graph.finite_incidenceSet {α : Type u} {β : Type v} (G : Graph α β) [Finite ↑G.edgeSet] (x : α) : (incidenceSet x).Finite

The incidence set of a vertex is finite when the graph has finitely many actual edges.

theorem Graph.finite_loopSet {α : Type u} {β : Type v} (G : Graph α β) [Finite ↑G.edgeSet] (x : α) : (loopSet x).Finite

The loop set of a vertex is finite when the graph has finitely many actual edges.

theorem Graph.nonloopIncidenceCount_add_ncard_loopSet {α : Type u} {β : Type v} (G : Graph α β) (x : α) (hfin : (incidenceSet x).Finite) : G.nonloopIncidenceCount x + (loopSet x).ncard = G.incidenceCount x

When the incidence set is finite, the incident edges split into the nonloop incident edges and the loops at the vertex.

@[simp]

theorem Graph.loopSet_eq_empty {α : Type u} {β : Type v} (G : Graph α β) [G.Loopless] (x : α) : loopSet x = ∅

A loopless multigraph has no loops at any vertex.

@[simp]

theorem Graph.nonloopIncidenceCount_eq_incidenceCount {α : Type u} {β : Type v} (G : Graph α β) [G.Loopless] (x : α) : G.nonloopIncidenceCount x = G.incidenceCount x

On a loopless multigraph, counting all incident edges is the same as counting nonloop incident edges.

@[simp]

theorem Graph.incidenceSet_deleteEdges {α : Type u} {β : Type v} (G : Graph α β) (F : Set β) (x : α) : incidenceSet x = incidenceSet x \ F

Deleting edges removes precisely the deleted members of a vertex's incidence set.

@[simp]

theorem Graph.loopSet_deleteEdges {α : Type u} {β : Type v} (G : Graph α β) (F : Set β) (x : α) : loopSet x = loopSet x \ F

Deleting edges removes precisely the deleted members of a vertex's loop set.

theorem Graph.incidenceCount_deleteEdges {α : Type u} {β : Type v} (G : Graph α β) (F : Set β) (x : α) : (G.deleteEdges F).incidenceCount x = (incidenceSet x \ F).ncard

The incidence count after edge deletion counts exactly the surviving incident edges.

theorem Graph.incidenceCount_deleteEdges_add_ncard_inter {α : Type u} {β : Type v} (G : Graph α β) (F : Set β) (x : α) (hfin : (incidenceSet x).Finite) : (G.deleteEdges F).incidenceCount x + (incidenceSet x ∩ F).ncard = G.incidenceCount x

When the incidence set is finite, the surviving and deleted incident-edge counts add to the original incidence count.

theorem Graph.nonloopIncidenceCount_deleteEdges {α : Type u} {β : Type v} (G : Graph α β) (F : Set β) (x : α) : (G.deleteEdges F).nonloopIncidenceCount x = ((incidenceSet x \ loopSet x) \ F).ncard

Deleting edges removes precisely the deleted members of a vertex's nonloop incidence set.

Basic examples

@[simp]

theorem Graph.incidenceSet_noEdge {α : Type u} {β : Type v} (X : Set α) (x : α) : incidenceSet x = ∅

A graph with no edges has an empty incidence set at every vertex.

@[simp]

theorem Graph.incidenceCount_noEdge {α : Type u} {β : Type v} (X : Set α) (x : α) : (noEdge X β).incidenceCount x = 0

A graph with no edges has incidence count zero at every vertex.

@[simp]

theorem Graph.incidenceSet_banana_left {α : Type u} {β : Type v} (x y : α) (E : Set β) : incidenceSet x = E

Every edge identity of a banana graph is incident to its left endpoint.

theorem Graph.incidenceSet_bouquet {α : Type u} {β : Type v} (x : α) (E : Set β) : incidenceSet x = E

Every edge identity of a bouquet is incident to its unique vertex.

@[simp]

theorem Graph.loopSet_bouquet {α : Type u} {β : Type v} (x : α) (E : Set β) : loopSet x = E

Every edge identity of a bouquet is a loop at its unique vertex.

@[simp]

theorem Graph.loopSet_banana_left {α : Type u} {β : Type v} (x y : α) (E : Set β) (hxy : x ≠ y) : loopSet x = ∅

A banana graph with distinct endpoints has no loops at its left endpoint.

@[simp]

theorem Graph.incidenceCount_banana_left {α : Type u} {β : Type v} (x y : α) (E : Set β) : (banana x y E).incidenceCount x = E.ncard

Every edge identity of a banana graph is incident to its left endpoint, so the incidence count there is E.ncard, which is zero when E is infinite.

theorem Graph.incidenceCount_bouquet {α : Type u} {β : Type v} (x : α) (E : Set β) : (bouquet x E).incidenceCount x = E.ncard

Every edge identity of a bouquet is a loop at its unique vertex, so its incidence count is E.ncard, which is zero when E is infinite.

@[simp]

theorem Graph.nonloopIncidenceCount_bouquet {α : Type u} {β : Type v} (x : α) (E : Set β) : (bouquet x E).nonloopIncidenceCount x = 0

A bouquet has no nonloop incident edges, independently of how many loops it has.

@[simp]

theorem Graph.nonloopIncidenceCount_banana_left {α : Type u} {β : Type v} (x y : α) (E : Set β) (hxy : x ≠ y) : (banana x y E).nonloopIncidenceCount x = E.ncard

When the endpoints of a banana graph are distinct, every edge is nonloop and the count at the left endpoint is E.ncard, which is zero when E is infinite.

noncomputable def Graph.internalEdges {α : Type u} {β : Type v} (G : Graph α β) [Fintype ↑G.edgeSet] (S : Finset ↑G.vertexSet) : Finset ↑G.edgeSet

The actual edge identities whose two endpoints both lie in S.

noncomputable def Graph.incidentEdges {α : Type u} {β : Type v} (G : Graph α β) [Fintype ↑G.edgeSet] (S : Finset ↑G.vertexSet) : Finset ↑G.edgeSet

The actual edge identities with at least one endpoint in S.

@[simp]

theorem Graph.mem_internalEdges {α : Type u} {β : Type v} (G : Graph α β) [Fintype ↑G.edgeSet] {S : Finset ↑G.vertexSet} {e : ↑G.edgeSet} : e ∈ G.internalEdges S ↔ ∃ x ∈ S, ∃ y ∈ S, G.IsLink ↑e ↑x ↑y

@[simp]

theorem Graph.mem_incidentEdges {α : Type u} {β : Type v} (G : Graph α β) [Fintype ↑G.edgeSet] {S : Finset ↑G.vertexSet} {e : ↑G.edgeSet} : e ∈ G.incidentEdges S ↔ ∃ x ∈ S, G.Inc ↑e ↑x

@[simp]

theorem Graph.internalEdges_empty {α : Type u} {β : Type v} (G : Graph α β) [Fintype ↑G.edgeSet] : G.internalEdges ∅ = ∅

@[simp]

theorem Graph.incidentEdges_empty {α : Type u} {β : Type v} (G : Graph α β) [Fintype ↑G.edgeSet] : G.incidentEdges ∅ = ∅

@[simp]

theorem Graph.incidentEdges_univ {α : Type u} {β : Type v} (G : Graph α β) [Fintype ↑G.edgeSet] [Fintype ↑G.vertexSet] : G.incidentEdges Finset.univ = Finset.univ

@[simp]

theorem Graph.internalEdges_univ {α : Type u} {β : Type v} (G : Graph α β) [Fintype ↑G.edgeSet] [Fintype ↑G.vertexSet] : G.internalEdges Finset.univ = Finset.univ

theorem Graph.internalEdges_subset_incidentEdges {α : Type u} {β : Type v} (G : Graph α β) [Fintype ↑G.edgeSet] (S : Finset ↑G.vertexSet) : G.internalEdges S ⊆ G.incidentEdges S

Every edge internal to S is incident with S.

theorem Graph.internalEdges_mono {α : Type u} {β : Type v} (G : Graph α β) [Fintype ↑G.edgeSet] {S T : Finset ↑G.vertexSet} (hST : S ⊆ T) : G.internalEdges S ⊆ G.internalEdges T

Enlarging a vertex set enlarges its set of internal edges.

theorem Graph.incidentEdges_mono {α : Type u} {β : Type v} (G : Graph α β) [Fintype ↑G.edgeSet] {S T : Finset ↑G.vertexSet} (hST : S ⊆ T) : G.incidentEdges S ⊆ G.incidentEdges T

Enlarging a vertex set enlarges its set of incident edges.

theorem Graph.incidentEdges_compl {α : Type u} {β : Type v} (G : Graph α β) [Fintype ↑G.edgeSet] [Fintype ↑G.vertexSet] [DecidableEq ↑G.vertexSet] [DecidableEq ↑G.edgeSet] (S : Finset ↑G.vertexSet) : (G.incidentEdges S)ᶜ = G.internalEdges Sᶜ

An edge has no end in S exactly when both of its ends lie in the complement of S.

theorem Graph.card_incidentEdges_add_card_internalEdges_compl {α : Type u} {β : Type v} (G : Graph α β) [Fintype ↑G.edgeSet] [Fintype ↑G.vertexSet] [DecidableEq ↑G.vertexSet] (S : Finset ↑G.vertexSet) : (G.incidentEdges S).card + (G.internalEdges Sᶜ).card = Fintype.card ↑G.edgeSet

Every actual edge is either incident with S or internal to its complement.

theorem Graph.card_incidentEdges_singleton {α : Type u} {β : Type v} (G : Graph α β) [Fintype ↑G.edgeSet] (x : ↑G.vertexSet) : (G.incidentEdges {x}).card = G.incidenceCount ↑x

The cardinality of the finite incident-edge set of a singleton is its incidence count.

theorem Graph.card_internalEdges_singleton {α : Type u} {β : Type v} (G : Graph α β) [Fintype ↑G.edgeSet] (x : ↑G.vertexSet) : (G.internalEdges {x}).card = (loopSet ↑x).ncard

The number of internal edges of a singleton is the number of loops at its vertex.

theorem Graph.sum_sum_incidentEdges_eq_sum_sum_filter_inc {α : Type u} {β : Type v} (G : Graph α β) [Fintype ↑G.edgeSet] {M : Type u_1} [AddCommMonoid M] [(e : β) → (x : α) → Decidable (G.Inc e x)] (S : Finset ↑G.vertexSet) (f : ↑G.edgeSet → M) : ∑ x ∈ S, ∑ e ∈ G.incidentEdges {x}, f e = ∑ e : ↑G.edgeSet, ∑ x ∈ S with G.Inc ↑e ↑x, f e

Summing over S the values of the edges incident with each vertex counts every actual edge once for each vertex of S incident with it.

instance Graph.instLooplessSym2OfSimpleGraph_tauCeti {α : Type u} (H : SimpleGraph α) : (ofSimpleGraph H).Loopless

The multigraph associated to a simple graph is loopless.

@[simp]

theorem Graph.inc_ofSimpleGraph {α : Type u} (H : SimpleGraph α) {e : Sym2 α} {x : α} : (ofSimpleGraph H).Inc e x ↔ e ∈ H.edgeSet ∧ x ∈ e

An edge of Graph.ofSimpleGraph H is incident to a vertex exactly when it is an edge of H containing that vertex.

@[simp]

theorem Graph.incidenceSet_ofSimpleGraph {α : Type u} (H : SimpleGraph α) (x : α) : incidenceSet x = H.incidenceSet x

The multigraph incidence set of Graph.ofSimpleGraph H is the usual simple-graph incidence set.

@[simp]

theorem Graph.incidenceCount_ofSimpleGraph {α : Type u} (H : SimpleGraph α) (x : α) [Fintype ↑(H.neighborSet x)] : (ofSimpleGraph H).incidenceCount x = H.degree x

The incidence count on Graph.ofSimpleGraph H is the degree in H.