Metamath Proof Explorer

Table of Contents - 16.2.9. Neighbors, complete graphs and universal vertices

1. Neighbors
   1. cnbgr
   2. df-nbgr
   3. nbgrprc0
   4. nbgrcl
   5. nbgrval
   6. dfnbgr2
   7. dfnbgr3
   8. nbgrnvtx0
   9. nbgrel
   10. nbgrisvtx
   11. nbgrssvtx
   12. nbuhgr
   13. nbupgr
   14. nbupgrel
   15. nbumgrvtx
   16. nbumgr
   17. nbusgrvtx
   18. nbusgr
   19. nbgr2vtx1edg
   20. nbuhgr2vtx1edgblem
   21. nbuhgr2vtx1edgb
   22. nbusgreledg
   23. uhgrnbgr0nb
   24. nbgr0vtxlem
   25. nbgr0vtx
   26. nbgr0edg
   27. nbgr1vtx
   28. nbgrnself
   29. nbgrnself2
   30. nbgrssovtx
   31. nbgrssvwo2
   32. nbgrsym
   33. nbupgrres
   34. usgrnbcnvfv
   35. nbusgredgeu
   36. edgnbusgreu
   37. nbusgredgeu0
   38. nbusgrf1o0
   39. nbusgrf1o1
   40. nbusgrf1o
   41. nbedgusgr
   42. edgusgrnbfin
   43. nbusgrfi
   44. nbfiusgrfi
   45. hashnbusgrnn0
   46. nbfusgrlevtxm1
   47. nbfusgrlevtxm2
   48. nbusgrvtxm1
   49. nb3grprlem1
   50. nb3grprlem2
   51. nb3grpr
   52. nb3grpr2
   53. nb3gr2nb
2. Universal vertices
   1. cuvtx
   2. df-uvtx
   3. uvtxval
   4. uvtxel
   5. uvtxisvtx
   6. uvtxssvtx
   7. vtxnbuvtx
   8. uvtxnbgrss
   9. uvtxnbgrvtx
   10. uvtx0
   11. isuvtx
   12. uvtxel1
   13. uvtx01vtx
   14. uvtx2vtx1edg
   15. uvtx2vtx1edgb
   16. uvtxnbgr
   17. uvtxnbgrb
   18. uvtxusgr
   19. uvtxusgrel
   20. uvtxnm1nbgr
   21. nbusgrvtxm1uvtx
   22. uvtxnbvtxm1
   23. nbupgruvtxres
   24. uvtxupgrres
3. Complete graphs
   1. ccplgr
   2. ccusgr
   3. df-cplgr
   4. df-cusgr
   5. cplgruvtxb
   6. prcliscplgr
   7. iscplgr
   8. iscplgrnb
   9. iscplgredg
   10. iscusgr
   11. cusgrusgr
   12. cusgrcplgr
   13. iscusgrvtx
   14. cusgruvtxb
   15. iscusgredg
   16. cusgredg
   17. cplgr0
   18. cusgr0
   19. cplgr0v
   20. cusgr0v
   21. cplgr1vlem
   22. cplgr1v
   23. cusgr1v
   24. cplgr2v
   25. cplgr2vpr
   26. nbcplgr
   27. cplgr3v
   28. cusgr3vnbpr
   29. cplgrop
   30. cusgrop
   31. cusgrexilem1
   32. usgrexilem
   33. usgrexi
   34. cusgrexilem2
   35. cusgrexi
   36. cusgrexg
   37. structtousgr
   38. structtocusgr
   39. cffldtocusgr
   40. cusgrres
   41. cusgrsizeindb0
   42. cusgrsizeindb1
   43. cusgrsizeindslem
   44. cusgrsizeinds
   45. cusgrsize2inds
   46. cusgrsize
   47. cusgrfilem1
   48. cusgrfilem2
   49. cusgrfilem3
   50. cusgrfi
   51. usgredgsscusgredg
   52. usgrsscusgr
   53. sizusglecusglem1
   54. sizusglecusglem2
   55. sizusglecusg
   56. fusgrmaxsize