Metamath Proof Explorer

Table of Contents - 16.4.16. Geometry in Euclidean spaces

1. Definition of the Euclidean space
   1. cee
   2. cbtwn
   3. ccgr
   4. df-ee
   5. df-btwn
   6. df-cgr
   7. elee
   8. mptelee
   9. mpteleeOLD
   10. eleenn
   11. eleei
   12. eedimeq
   13. brbtwn
   14. brcgr
   15. fveere
   16. fveecn
   17. eqeefv
   18. eqeelen
   19. brbtwn2
   20. colinearalglem1
   21. colinearalglem2
   22. colinearalglem3
   23. colinearalglem4
   24. colinearalg
   25. eleesub
   26. eleesubd
2. Tarski's axioms for geometry for the Euclidean space
   1. axdimuniq
   2. axcgrrflx
   3. axcgrtr
   4. axcgrid
   5. axsegconlem1
   6. axsegconlem2
   7. axsegconlem3
   8. axsegconlem4
   9. axsegconlem5
   10. axsegconlem6
   11. axsegconlem7
   12. axsegconlem8
   13. axsegconlem9
   14. axsegconlem10
   15. axsegcon
   16. ax5seglem1
   17. ax5seglem2
   18. ax5seglem3a
   19. ax5seglem3
   20. ax5seglem4
   21. ax5seglem5
   22. ax5seglem6
   23. ax5seglem7
   24. ax5seglem8
   25. ax5seglem9
   26. ax5seg
   27. axbtwnid
   28. axpaschlem
   29. axpasch
   30. axlowdimlem1
   31. axlowdimlem2
   32. axlowdimlem3
   33. axlowdimlem4
   34. axlowdimlem5
   35. axlowdimlem6
   36. axlowdimlem7
   37. axlowdimlem8
   38. axlowdimlem9
   39. axlowdimlem10
   40. axlowdimlem11
   41. axlowdimlem12
   42. axlowdimlem13
   43. axlowdimlem14
   44. axlowdimlem15
   45. axlowdimlem16
   46. axlowdimlem17
   47. axlowdim1
   48. axlowdim2
   49. axlowdim
   50. axeuclidlem
   51. axeuclid
   52. axcontlem1
   53. axcontlem2
   54. axcontlem3
   55. axcontlem4
   56. axcontlem5
   57. axcontlem6
   58. axcontlem7
   59. axcontlem8
   60. axcontlem9
   61. axcontlem10
   62. axcontlem11
   63. axcontlem12
   64. axcont
3. EE^n fulfills Tarski's Axioms
   1. ceeng
   2. df-eeng
   3. eengv
   4. eengstr
   5. eengbas
   6. ebtwntg
   7. ecgrtg
   8. elntg
   9. elntg2
   10. eengtrkg
   11. eengtrkge