Metamath Proof Explorer

Table of Contents - 16.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. slotsinbpsd
16. slotslnbpsd
17. lngndxnitvndx
18. trkgstr
19. trkgbas
20. trkgdist
21. trkgitv
22. df-trkgc
23. df-trkgb
24. df-trkgcb
25. df-trkge
26. df-trkgld
27. df-trkg
28. istrkgc
29. istrkgb
30. istrkgcb
31. istrkge
32. istrkgl
33. istrkgld
34. istrkg2ld
35. istrkg3ld
36. axtgcgrrflx
37. axtgcgrid
38. axtgsegcon
39. axtg5seg
40. axtgbtwnid
41. axtgpasch
42. axtgcont1
43. axtgcont
44. axtglowdim2
45. axtgupdim2
46. axtgeucl
47. Justification for the congruence notation
    1. tgjustf
    2. tgjustr
    3. tgjustc1
    4. tgjustc2