Description: The number of vertices of odd degree is even in a finite simple graph. Proposition 1.2.1 in Diestel p. 5. See also remark about equation (2) in section I.1 in Bollobas p. 4. (Contributed by AV, 27-Dec-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | finsumvtxdgeven.v | |- V = ( Vtx ` G ) |
|
| finsumvtxdgeven.i | |- I = ( iEdg ` G ) |
||
| finsumvtxdgeven.d | |- D = ( VtxDeg ` G ) |
||
| Assertion | fusgrvtxdgonume | |- ( G e. FinUSGraph -> 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | finsumvtxdgeven.v | |- V = ( Vtx ` G ) |
|
| 2 | finsumvtxdgeven.i | |- I = ( iEdg ` G ) |
|
| 3 | finsumvtxdgeven.d | |- D = ( VtxDeg ` G ) |
|
| 4 | 1 2 | fusgrfupgrfs | |- ( G e. FinUSGraph -> ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) ) |
| 5 | 1 2 3 | vtxdgoddnumeven | |- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) |
| 6 | 4 5 | syl | |- ( G e. FinUSGraph -> 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) |