Metamath Proof Explorer

Table of Contents - 16.5. The Friendship Theorem

1. Friendship graphs - basics
   1. cfrgr
   2. df-frgr
   3. isfrgr
   4. frgrusgr
   5. frgr0v
   6. frgr0vb
   7. frgruhgr0v
   8. frgr0
   9. frcond1
   10. frcond2
   11. frgreu
   12. frcond3
   13. frcond4
2. The friendship theorem for small graphs
   1. frgr1v
   2. nfrgr2v
   3. frgr3vlem1
   4. frgr3vlem2
   5. frgr3v
   6. 1vwmgr
   7. 3vfriswmgrlem
   8. 3vfriswmgr
   9. 1to2vfriswmgr
   10. 1to3vfriswmgr
   11. 1to3vfriendship
3. Theorems according to Mertzios and Unger
   1. 2pthfrgrrn
   2. 2pthfrgrrn2
   3. 2pthfrgr
   4. 3cyclfrgrrn1
   5. 3cyclfrgrrn
   6. 3cyclfrgrrn2
   7. 3cyclfrgr
   8. 4cycl2v2nb
   9. 4cycl2vnunb
   10. n4cyclfrgr
   11. 4cyclusnfrgr
   12. frgrnbnb
   13. frgrconngr
   14. vdgn0frgrv2
   15. vdgn1frgrv2
   16. vdgn1frgrv3
   17. vdgfrgrgt2
4. Huneke's Proof of the Friendship Theorem
   1. frgrncvvdeqlem1
   2. frgrncvvdeqlem2
   3. frgrncvvdeqlem3
   4. frgrncvvdeqlem4
   5. frgrncvvdeqlem5
   6. frgrncvvdeqlem6
   7. frgrncvvdeqlem7
   8. frgrncvvdeqlem8
   9. frgrncvvdeqlem9
   10. frgrncvvdeqlem10
   11. frgrncvvdeq
   12. frgrwopreglem4a
   13. frgrwopreglem5a
   14. frgrwopreglem1
   15. frgrwopreglem2
   16. frgrwopreglem3
   17. frgrwopreglem4
   18. frgrwopregasn
   19. frgrwopregbsn
   20. frgrwopreg1
   21. frgrwopreg2
   22. frgrwopreglem5lem
   23. frgrwopreglem5
   24. frgrwopreglem5ALT
   25. frgrwopreg
   26. frgrregorufr0
   27. frgrregorufr
   28. frgrregorufrg
   29. frgr2wwlkeu
   30. frgr2wwlkn0
   31. frgr2wwlk1
   32. frgr2wsp1
   33. frgr2wwlkeqm
   34. frgrhash2wsp
   35. fusgreg2wsplem
   36. fusgr2wsp2nb
   37. fusgreghash2wspv
   38. fusgreg2wsp
   39. 2wspmdisj
   40. fusgreghash2wsp
   41. frrusgrord0lem
   42. frrusgrord0
   43. frrusgrord
   44. numclwwlk2lem1lem
   45. 2clwwlklem
   46. clwwnrepclwwn
   47. clwwnonrepclwwnon
   48. 2clwwlk2clwwlklem
   49. 2clwwlk
   50. 2clwwlk2
   51. 2clwwlkel
   52. 2clwwlk2clwwlk
   53. numclwwlk1lem2foalem
   54. extwwlkfab
   55. extwwlkfabel
   56. numclwwlk1lem2foa
   57. numclwwlk1lem2f
   58. numclwwlk1lem2fv
   59. numclwwlk1lem2f1
   60. numclwwlk1lem2fo
   61. numclwwlk1lem2f1o
   62. numclwwlk1lem2
   63. numclwwlk1
   64. clwwlknonclwlknonf1o
   65. clwwlknonclwlknonen
   66. dlwwlknondlwlknonf1olem1
   67. dlwwlknondlwlknonf1o
   68. dlwwlknondlwlknonen
   69. wlkl0
   70. clwlknon2num
   71. numclwlk1lem1
   72. numclwlk1lem2
   73. numclwlk1
   74. numclwwlkovh0
   75. numclwwlkovh
   76. numclwwlkovq
   77. numclwwlkqhash
   78. numclwwlk2lem1
   79. numclwlk2lem2f
   80. numclwlk2lem2fv
   81. numclwlk2lem2f1o
   82. numclwwlk2lem3
   83. numclwwlk2
   84. numclwwlk3lem1
   85. numclwwlk3lem2lem
   86. numclwwlk3lem2
   87. numclwwlk3
   88. numclwwlk4
   89. numclwwlk5lem
   90. numclwwlk5
   91. numclwwlk7lem
   92. numclwwlk6
   93. numclwwlk7
   94. numclwwlk8
   95. frgrreggt1
   96. frgrreg
   97. frgrregord013
   98. frgrregord13
   99. frgrogt3nreg
   100. friendshipgt3
   101. friendship