Metamath Proof Explorer

Table of Contents - 20.10.37. Geometry in the Euclidean space

1. Congruence properties
   1. cofs
   2. df-ofs
   3. cgrrflx2d
   4. cgrtr4d
   5. cgrtr4and
   6. cgrrflx
   7. cgrrflxd
   8. cgrcomim
   9. cgrcom
   10. cgrcomand
   11. cgrtr
   12. cgrtrand
   13. cgrtr3
   14. cgrtr3and
   15. cgrcoml
   16. cgrcomr
   17. cgrcomlr
   18. cgrcomland
   19. cgrcomrand
   20. cgrcomlrand
   21. cgrtriv
   22. cgrid2
   23. cgrdegen
   24. brofs
   25. 5segofs
   26. ofscom
   27. cgrextend
   28. cgrextendand
   29. segconeq
   30. segconeu
2. Betweenness properties
   1. btwntriv2
   2. btwncomim
   3. btwncom
   4. btwncomand
   5. btwntriv1
   6. btwnswapid
   7. btwnswapid2
   8. btwnintr
   9. btwnexch3
   10. btwnexch3and
   11. btwnouttr2
   12. btwnexch2
   13. btwnouttr
   14. btwnexch
   15. btwnexchand
   16. btwndiff
   17. trisegint
3. Segment Transportation
   1. ctransport
   2. df-transport
   3. funtransport
   4. fvtransport
   5. transportcl
   6. transportprops
4. Properties relating betweenness and congruence
   1. cifs
   2. ccgr3
   3. ccolin
   4. cfs
   5. df-colinear
   6. df-ifs
   7. df-cgr3
   8. df-fs
   9. brifs
   10. ifscgr
   11. cgrsub
   12. brcgr3
   13. cgr3permute3
   14. cgr3permute1
   15. cgr3permute2
   16. cgr3permute4
   17. cgr3permute5
   18. cgr3tr4
   19. cgr3com
   20. cgr3rflx
   21. cgrxfr
   22. btwnxfr
   23. colinrel
   24. brcolinear2
   25. brcolinear
   26. colinearex
   27. colineardim1
   28. colinearperm1
   29. colinearperm3
   30. colinearperm2
   31. colinearperm4
   32. colinearperm5
   33. colineartriv1
   34. colineartriv2
   35. btwncolinear1
   36. btwncolinear2
   37. btwncolinear3
   38. btwncolinear4
   39. btwncolinear5
   40. btwncolinear6
   41. colinearxfr
   42. lineext
   43. brofs2
   44. brifs2
   45. brfs
   46. fscgr
   47. linecgr
   48. linecgrand
   49. lineid
   50. idinside
   51. endofsegid
   52. endofsegidand
5. Connectivity of betweenness
   1. btwnconn1lem1
   2. btwnconn1lem2
   3. btwnconn1lem3
   4. btwnconn1lem4
   5. btwnconn1lem5
   6. btwnconn1lem6
   7. btwnconn1lem7
   8. btwnconn1lem8
   9. btwnconn1lem9
   10. btwnconn1lem10
   11. btwnconn1lem11
   12. btwnconn1lem12
   13. btwnconn1lem13
   14. btwnconn1lem14
   15. btwnconn1
   16. btwnconn2
   17. btwnconn3
   18. midofsegid
   19. segcon2
6. Segment less than or equal to
   1. csegle
   2. df-segle
   3. brsegle
   4. brsegle2
   5. seglecgr12im
   6. seglecgr12
   7. seglerflx
   8. seglemin
   9. segletr
   10. segleantisym
   11. seglelin
   12. btwnsegle
   13. colinbtwnle
7. Outside-of relationship
   1. coutsideof
   2. df-outsideof
   3. broutsideof
   4. broutsideof2
   5. outsidene1
   6. outsidene2
   7. btwnoutside
   8. broutsideof3
   9. outsideofrflx
   10. outsideofcom
   11. outsideoftr
   12. outsideofeq
   13. outsideofeu
   14. outsidele
   15. outsideofcol
8. Lines and Rays
   1. cline2
   2. cray
   3. clines2
   4. df-line2
   5. df-ray
   6. df-lines2
   7. funray
   8. fvray
   9. funline
   10. linedegen
   11. fvline
   12. liness
   13. fvline2
   14. lineunray
   15. lineelsb2
   16. linerflx1
   17. linecom
   18. linerflx2
   19. ellines
   20. linethru
   21. hilbert1.1
   22. hilbert1.2
   23. linethrueu
   24. lineintmo