Metamath Proof Explorer

Table of Contents - 15.1. Definition and Tarski's Axioms of Geometry

  1. cstrkg
  2. cstrkgc
  3. cstrkgb
  4. cstrkgcb
  5. cstrkgld
  6. cstrkge
  7. citv
  8. clng
  9. df-itv
  10. df-lng
  11. itvndx
  12. lngndx
  13. itvid
  14. lngid
  15. trkgstr
  16. trkgbas
  17. trkgdist
  18. trkgitv
  19. df-trkgc
  20. df-trkgb
  21. df-trkgcb
  22. df-trkge
  23. df-trkgld
  24. df-trkg
  25. istrkgc
  26. istrkgb
  27. istrkgcb
  28. istrkge
  29. istrkgl
  30. istrkgld
  31. istrkg2ld
  32. istrkg3ld
  33. axtgcgrrflx
  34. axtgcgrid
  35. axtgsegcon
  36. axtg5seg
  37. axtgbtwnid
  38. axtgpasch
  39. axtgcont1
  40. axtgcont
  41. axtglowdim2
  42. axtgupdim2
  43. axtgeucl
  44. Justification for the congruence notation
    1. tgjustf
    2. tgjustr
    3. tgjustc1
    4. tgjustc2