Metamath Proof Explorer

Table of Contents - 20.16.8. Affine, Euclidean, and Cartesian geometry

A few basic theorems to start affine, Euclidean, and Cartesian geometry.

The first step is to define real vector spaces, then barycentric coordinates and convex hulls.

1. Real vector spaces
   1. bj-fvimacnv0
   2. bj-isvec
   3. bj-fldssdrng
   4. bj-flddrng
   5. bj-rrdrg
   6. bj-isclm
   7. crrvec
   8. df-bj-rvec
   9. bj-isrvec
   10. bj-rvecmod
   11. bj-rvecssmod
   12. bj-rvecrr
   13. bj-isrvecd
   14. bj-rvecvec
   15. bj-isrvec2
   16. bj-rvecssvec
   17. bj-rveccmod
   18. bj-rvecsscmod
   19. bj-rvecsscvec
   20. bj-rveccvec
   21. bj-rvecssabl
   22. bj-rvecabl
2. Complex numbers (supplements)
   1. bj-subcom
   2. bj-lineqi
3. Barycentric coordinates
   1. bj-bary1lem
   2. bj-bary1lem1
   3. bj-bary1