Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-vdgr Structured version   Unicode version

Definition df-vdgr 21665
 Description: Define the vertex degree function (for an undirected multigraph). To be appropriate for multigraphs, we have to double-count those edges that contain "twice" (i.e. self-loops), this being represented as a singleton as the edge's value. Since the degree of a vertex can be (positive) infinity (if the graph containing the vertex is not of finite size), the extended addition is used for the summation of the number of "ordinary" edges" and the number of "loops". (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.)
Assertion
Ref Expression
df-vdgr VDeg
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-vdgr
StepHypRef Expression
1 cvdg 21664 . 2 VDeg
2 vv . . 3
3 ve . . 3
4 cvv 2956 . . 3
5 vu . . . 4
62cv 1651 . . . 4
75cv 1651 . . . . . . . 8
8 vx . . . . . . . . . 10
98cv 1651 . . . . . . . . 9
103cv 1651 . . . . . . . . 9
119, 10cfv 5454 . . . . . . . 8
127, 11wcel 1725 . . . . . . 7
1310cdm 4878 . . . . . . 7
1412, 8, 13crab 2709 . . . . . 6
15 chash 11618 . . . . . 6
1614, 15cfv 5454 . . . . 5
177csn 3814 . . . . . . . 8
1811, 17wceq 1652 . . . . . . 7
1918, 8, 13crab 2709 . . . . . 6
2019, 15cfv 5454 . . . . 5
21 cxad 10708 . . . . 5
2216, 20, 21co 6081 . . . 4
235, 6, 22cmpt 4266 . . 3
242, 3, 4, 4, 23cmpt2 6083 . 2
251, 24wceq 1652 1 VDeg
 Colors of variables: wff set class This definition is referenced by:  vdgrfval  21666
 Copyright terms: Public domain W3C validator