Metamath Proof Explorer

Table of Contents - 17.3.4. Paths and simple paths

  1. cpths
  2. cspths
  3. cpthson
  4. cspthson
  5. df-pths
  6. df-spths
  7. df-pthson
  8. df-spthson
  9. relpths
  10. pthsfval
  11. spthsfval
  12. ispth
  13. isspth
  14. pthistrl
  15. spthispth
  16. pthiswlk
  17. spthiswlk
  18. pthdivtx
  19. pthdadjvtx
  20. 2pthnloop
  21. upgr2pthnlp
  22. spthdifv
  23. spthdep
  24. pthdepisspth
  25. upgrwlkdvdelem
  26. upgrwlkdvde
  27. upgrspthswlk
  28. upgrwlkdvspth
  29. pthsonfval
  30. spthson
  31. ispthson
  32. isspthson
  33. pthsonprop
  34. spthonprop
  35. pthonispth
  36. pthontrlon
  37. pthonpth
  38. isspthonpth
  39. spthonisspth
  40. spthonpthon
  41. spthonepeq
  42. uhgrwkspthlem1
  43. uhgrwkspthlem2
  44. uhgrwkspth
  45. usgr2wlkneq
  46. usgr2wlkspthlem1
  47. usgr2wlkspthlem2
  48. usgr2wlkspth
  49. usgr2trlncl
  50. usgr2trlspth
  51. usgr2pthspth
  52. usgr2pthlem
  53. usgr2pth
  54. usgr2pth0
  55. pthdlem1
  56. pthdlem2lem
  57. pthdlem2
  58. pthd