Metamath Proof Explorer

Table of Contents - 20.25.7. Atoms, hyperplanes, and covering in a left vector space (or module)

1. clsa
2. clsh
3. df-lsatoms
4. df-lshyp
5. lshpset
6. islshp
7. islshpsm
8. lshplss
9. lshpne
10. lshpnel
11. lshpnelb
12. lshpnel2N
13. lshpne0
14. lshpdisj
15. lshpcmp
16. lshpinN
17. lsatset
18. islsat
19. lsatlspsn2
20. lsatlspsn
21. islsati
22. lsateln0
23. lsatlss
24. lsatlssel
25. lsatssv
26. lsatn0
27. lsatspn0
28. lsator0sp
29. lsatssn0
30. lsatcmp
31. lsatcmp2
32. lsatel
33. lsatelbN
34. lsat2el
35. lsmsat
36. lsatfixedN
37. lsmsatcv
38. lssatomic
39. lssats
40. lpssat
41. lrelat
42. lssatle
43. lssat
44. islshpat
45. clcv
46. df-lcv
47. lcvfbr
48. lcvbr
49. lcvbr2
50. lcvbr3
51. lcvpss
52. lcvnbtwn
53. lcvntr
54. lcvnbtwn2
55. lcvnbtwn3
56. lsmcv2
57. lcvat
58. lsatcv0
59. lsatcveq0
60. lsat0cv
61. lcvexchlem1
62. lcvexchlem2
63. lcvexchlem3
64. lcvexchlem4
65. lcvexchlem5
66. lcvexch
67. lcvp
68. lcv1
69. lcv2
70. lsatexch
71. lsatnle
72. lsatnem0
73. lsatexch1
74. lsatcv0eq
75. lsatcv1
76. lsatcvatlem
77. lsatcvat
78. lsatcvat2
79. lsatcvat3
80. islshpcv
81. l1cvpat
82. l1cvat
83. lshpat