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