Metamath Proof Explorer

Table of Contents - 15.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. eleenn
   10. eleei
   11. eedimeq
   12. brbtwn
   13. brcgr
   14. fveere
   15. fveecn
   16. eqeefv
   17. eqeelen
   18. brbtwn2
   19. colinearalglem1
   20. colinearalglem2
   21. colinearalglem3
   22. colinearalglem4
   23. colinearalg
   24. eleesub
   25. 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