Metamath Proof Explorer

Table of Contents - 16.2. Undirected graphs

For undirected graphs, we will have the following hierarchy/taxonomy:

* Undirected Hypergraph:

* Undirected loop-free graphs: ULFGraph (not defined formally yet)

* Undirected simple Hypergraph: => (ushgruhgr)

* Undirected Pseudograph: => (upgruhgr)

* Undirected loop-free hypergraph: ULFHGraph (not defined formally yet) => ULFHGraph and ULFHGraph ULFGraph

* Undirected loop-free simple hypergraph: ULFSHGraph (not defined formally yet) => ULFSHGraph and ULFSHGraph ULFHGraph

* Undirected simple Pseudograph: => (uspgrupgr) and (uspgrushgr), see also uspgrupgrushgr

* Undirected Muligraph: => (umgrupgr) and ULFHGraph (umgrislfupgr)

* Undirected simple Graph: => (usgruspgr) and (usgrumgr) and ULFSHGraph (usgrislfuspgr) see also usgrumgruspgr

1. Undirected hypergraphs
   1. cuhgr
   2. cushgr
   3. df-uhgr
   4. df-ushgr
   5. isuhgr
   6. isushgr
   7. uhgrf
   8. ushgrf
   9. uhgrss
   10. uhgreq12g
   11. uhgrfun
   12. uhgrn0
   13. lpvtx
   14. ushgruhgr
   15. isuhgrop
   16. uhgr0e
   17. uhgr0vb
   18. uhgr0
   19. uhgrun
   20. uhgrunop
   21. ushgrun
   22. ushgrunop
   23. uhgrstrrepe
   24. incistruhgr
2. Undirected pseudographs and multigraphs
   1. cupgr
   2. cumgr
   3. df-upgr
   4. df-umgr
   5. isupgr
   6. wrdupgr
   7. upgrf
   8. upgrfn
   9. upgrss
   10. upgrn0
   11. upgrle
   12. upgrfi
   13. upgrex
   14. upgrbi
   15. upgrop
   16. isumgr
   17. isumgrs
   18. wrdumgr
   19. umgrf
   20. umgrfn
   21. umgredg2
   22. umgrbi
   23. upgruhgr
   24. umgrupgr
   25. umgruhgr
   26. upgrle2
   27. umgrnloopv
   28. umgredgprv
   29. umgrnloop
   30. umgrnloop0
   31. umgr0e
   32. upgr0e
   33. upgr1elem
   34. upgr1e
   35. upgr0eop
   36. upgr1eop
   37. upgr0eopALT
   38. upgr1eopALT
   39. upgrun
   40. upgrunop
   41. umgrun
   42. umgrunop
3. Loop-free graphs
   1. umgrislfupgrlem
   2. umgrislfupgr
   3. lfgredgge2
   4. lfgrnloop
4. Edges as subsets of vertices of graphs
   1. uhgredgiedgb
   2. uhgriedg0edg0
   3. uhgredgn0
   4. edguhgr
   5. uhgredgrnv
   6. uhgredgss
   7. upgredgss
   8. umgredgss
   9. edgupgr
   10. edgumgr
   11. uhgrvtxedgiedgb
   12. upgredg
   13. umgredg
   14. upgrpredgv
   15. umgrpredgv
   16. upgredg2vtx
   17. upgredgpr
   18. edglnl
   19. numedglnl
   20. umgredgne
   21. umgrnloop2
   22. umgredgnlp
5. Undirected simple graphs
   1. cuspgr
   2. cusgr
   3. df-uspgr
   4. df-usgr
   5. isuspgr
   6. isusgr
   7. uspgrf
   8. usgrf
   9. isusgrs
   10. usgrfs
   11. usgrfun
   12. usgredgss
   13. edgusgr
   14. isuspgrop
   15. isusgrop
   16. usgrop
   17. isausgr
   18. ausgrusgrb
   19. usgrausgri
   20. ausgrumgri
   21. ausgrusgri
   22. usgrausgrb
   23. usgredgop
   24. usgrf1o
   25. usgrf1
   26. uspgrf1oedg
   27. usgrss
   28. uspgrushgr
   29. uspgrupgr
   30. uspgrupgrushgr
   31. usgruspgr
   32. usgrumgr
   33. usgrumgruspgr
   34. usgruspgrb
   35. usgrupgr
   36. usgruhgr
   37. usgrislfuspgr
   38. uspgrun
   39. uspgrunop
   40. usgrun
   41. usgrunop
   42. usgredg2
   43. usgredg2ALT
   44. usgredgprv
   45. usgredgprvALT
   46. usgredgppr
   47. usgrpredgv
   48. edgssv2
   49. usgredg
   50. usgrnloopv
   51. usgrnloopvALT
   52. usgrnloop
   53. usgrnloopALT
   54. usgrnloop0
   55. usgrnloop0ALT
   56. usgredgne
   57. usgrf1oedg
   58. uhgr2edg
   59. umgr2edg
   60. usgr2edg
   61. umgr2edg1
   62. usgr2edg1
   63. umgrvad2edg
   64. umgr2edgneu
   65. usgrsizedg
   66. usgredg3
   67. usgredg4
   68. usgredgreu
   69. usgredg2vtx
   70. uspgredg2vtxeu
   71. usgredg2vtxeu
   72. usgredg2vtxeuALT
   73. uspgredg2vlem
   74. uspgredg2v
   75. usgredg2vlem1
   76. usgredg2vlem2
   77. usgredg2v
   78. usgriedgleord
   79. ushgredgedg
   80. usgredgedg
   81. ushgredgedgloop
   82. uspgredgleord
   83. usgredgleord
   84. usgredgleordALT
   85. usgrstrrepe
6. Examples for graphs
   1. usgr0e
   2. usgr0vb
   3. uhgr0v0e
   4. uhgr0vsize0
   5. uhgr0edgfi
   6. usgr0v
   7. uhgr0vusgr
   8. usgr0
   9. uspgr1e
   10. usgr1e
   11. usgr0eop
   12. uspgr1eop
   13. uspgr1ewop
   14. uspgr1v1eop
   15. usgr1eop
   16. uspgr2v1e2w
   17. usgr2v1e2w
   18. edg0usgr
   19. lfuhgr1v0e
   20. usgr1vr
   21. usgr1v
   22. usgr1v0edg
   23. usgrexmpldifpr
   24. usgrexmplef
   25. usgrexmpllem
   26. usgrexmplvtx
   27. usgrexmpledg
   28. usgrexmpl
   29. griedg0prc
   30. griedg0ssusgr
   31. usgrprc
7. Subgraphs
   1. csubgr
   2. df-subgr
   3. relsubgr
   4. subgrv
   5. issubgr
   6. issubgr2
   7. subgrprop
   8. subgrprop2
   9. uhgrissubgr
   10. subgrprop3
   11. egrsubgr
   12. 0grsubgr
   13. 0uhgrsubgr
   14. uhgrsubgrself
   15. subgrfun
   16. subgruhgrfun
   17. subgreldmiedg
   18. subgruhgredgd
   19. subumgredg2
   20. subuhgr
   21. subupgr
   22. subumgr
   23. subusgr
   24. uhgrspansubgrlem
   25. uhgrspansubgr
   26. uhgrspan
   27. upgrspan
   28. umgrspan
   29. usgrspan
   30. uhgrspanop
   31. upgrspanop
   32. umgrspanop
   33. usgrspanop
   34. uhgrspan1lem1
   35. uhgrspan1lem2
   36. uhgrspan1lem3
   37. uhgrspan1
   38. upgrreslem
   39. umgrreslem
   40. upgrres
   41. umgrres
   42. usgrres
   43. upgrres1lem1
   44. umgrres1lem
   45. upgrres1lem2
   46. upgrres1lem3
   47. upgrres1
   48. umgrres1
   49. usgrres1
8. Finite undirected simple graphs
   1. cfusgr
   2. df-fusgr
   3. isfusgr
   4. fusgrvtxfi
   5. isfusgrf1
   6. isfusgrcl
   7. fusgrusgr
   8. opfusgr
   9. usgredgffibi
   10. fusgredgfi
   11. usgr1v0e
   12. usgrfilem
   13. fusgrfisbase
   14. fusgrfisstep
   15. fusgrfis
   16. fusgrfupgrfs
9. Neighbors, complete graphs and universal vertices
   1. Neighbors
   2. Universal vertices
   3. Complete graphs
10. Vertex degree
    1. cvtxdg
    2. df-vtxdg
    3. vtxdgfval
    4. vtxdgval
    5. vtxdgfival
    6. vtxdgop
    7. vtxdgf
    8. vtxdgelxnn0
    9. vtxdg0v
    10. vtxdg0e
    11. vtxdgfisnn0
    12. vtxdgfisf
    13. vtxdeqd
    14. vtxduhgr0e
    15. vtxdlfuhgr1v
    16. vdumgr0
    17. vtxdun
    18. vtxdfiun
    19. vtxduhgrun
    20. vtxduhgrfiun
    21. vtxdlfgrval
    22. vtxdumgrval
    23. vtxdusgrval
    24. vtxd0nedgb
    25. vtxdushgrfvedglem
    26. vtxdushgrfvedg
    27. vtxdusgrfvedg
    28. vtxduhgr0nedg
    29. vtxdumgr0nedg
    30. vtxduhgr0edgnel
    31. vtxdusgr0edgnel
    32. vtxdusgr0edgnelALT
    33. vtxdgfusgrf
    34. vtxdgfusgr
    35. fusgrn0degnn0
    36. 1loopgruspgr
    37. 1loopgredg
    38. 1loopgrnb0
    39. 1loopgrvd2
    40. 1loopgrvd0
    41. 1hevtxdg0
    42. 1hevtxdg1
    43. 1hegrvtxdg1
    44. 1hegrvtxdg1r
    45. 1egrvtxdg1
    46. 1egrvtxdg1r
    47. 1egrvtxdg0
    48. p1evtxdeqlem
    49. p1evtxdeq
    50. p1evtxdp1
    51. uspgrloopvtx
    52. uspgrloopvtxel
    53. uspgrloopiedg
    54. uspgrloopedg
    55. uspgrloopnb0
    56. uspgrloopvd2
    57. umgr2v2evtx
    58. umgr2v2evtxel
    59. umgr2v2eiedg
    60. umgr2v2eedg
    61. umgr2v2e
    62. umgr2v2enb1
    63. umgr2v2evd2
    64. hashnbusgrvd
    65. usgruvtxvdb
    66. vdiscusgrb
    67. vdiscusgr
    68. vtxdusgradjvtx
    69. usgrvd0nedg
    70. uhgrvd00
    71. usgrvd00
    72. vdegp1ai
    73. vdegp1bi
    74. vdegp1ci
    75. vtxdginducedm1lem1
    76. vtxdginducedm1lem2
    77. vtxdginducedm1lem3
    78. vtxdginducedm1lem4
    79. vtxdginducedm1
    80. vtxdginducedm1fi
    81. finsumvtxdg2ssteplem1
    82. finsumvtxdg2ssteplem2
    83. finsumvtxdg2ssteplem3
    84. finsumvtxdg2ssteplem4
    85. finsumvtxdg2sstep
    86. finsumvtxdg2size
    87. fusgr1th
    88. finsumvtxdgeven
    89. vtxdgoddnumeven
    90. fusgrvtxdgonume
11. Regular graphs
    1. crgr
    2. crusgr
    3. df-rgr
    4. df-rusgr
    5. isrgr
    6. rgrprop
    7. isrusgr
    8. rusgrprop
    9. rusgrrgr
    10. rusgrusgr
    11. finrusgrfusgr
    12. isrusgr0
    13. rusgrprop0
    14. usgreqdrusgr
    15. fusgrregdegfi
    16. fusgrn0eqdrusgr
    17. frusgrnn0
    18. 0edg0rgr
    19. uhgr0edg0rgr
    20. uhgr0edg0rgrb
    21. usgr0edg0rusgr
    22. 0vtxrgr
    23. 0vtxrusgr
    24. 0uhgrrusgr
    25. 0grrusgr
    26. 0grrgr
    27. cusgrrusgr
    28. cusgrm1rusgr
    29. rusgrpropnb
    30. rusgrpropedg
    31. rusgrpropadjvtx
    32. rusgrnumwrdl2
    33. rusgr1vtxlem
    34. rusgr1vtx
    35. rgrusgrprc
    36. rusgrprc
    37. rgrprc
    38. rgrprcx
    39. rgrx0ndm
    40. rgrx0nd