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

Definition df-vdgr 25607
 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 25606 . 2 VDeg
2 vv . . 3
3 ve . . 3
4 cvv 3081 . . 3
5 vu . . . 4
62cv 1436 . . . 4
75cv 1436 . . . . . . . 8
8 vx . . . . . . . . . 10
98cv 1436 . . . . . . . . 9
103cv 1436 . . . . . . . . 9
119, 10cfv 5597 . . . . . . . 8
127, 11wcel 1868 . . . . . . 7
1310cdm 4849 . . . . . . 7
1412, 8, 13crab 2779 . . . . . 6
15 chash 12514 . . . . . 6
1614, 15cfv 5597 . . . . 5
177csn 3996 . . . . . . . 8
1811, 17wceq 1437 . . . . . . 7
1918, 8, 13crab 2779 . . . . . 6
2019, 15cfv 5597 . . . . 5
21 cxad 11407 . . . . 5
2216, 20, 21co 6301 . . . 4
235, 6, 22cmpt 4479 . . 3
242, 3, 4, 4, 23cmpt2 6303 . 2
251, 24wceq 1437 1 VDeg
 Colors of variables: wff setvar class This definition is referenced by:  vdgrfval  25608
 Copyright terms: Public domain W3C validator