1 r2vK
2 r2v_inj
3 v2rK
4 v2r_inj
5 b2mxK
6 gen_vs2mx
7 vs2mxK
8 mx2vsK
9 memvE
10 vlineP
11 mem0v
12 memvN
13 memvD
14 memvB
15 memvZ
16 memv_suml
17 memv_line
18 subvP
19 subv_refl
20 subv_trans
21 subv_anti
22 eqEsubv
23 subvPn
24 sub0v
25 subv0
26 memv0
27 subvf
28 memvf
29 memv_pick
30 vpick0
31 subv_add
32 addvS
33 addvSl
34 addvSr
35 addvC
36 addvA
37 addv_idPl
38 addv_idPr
39 addvv
40 add0v
41 addv0
42 sumfv
43 addvf
44 memv_add
45 memv_addP
46 sumv_sup
47 subv_sumP
48 memv_sumr
49 memv_sumP
50 subv_cap
51 capvS
52 capvSl
53 capvSr
54 capvC
55 capvA
56 capv_idPl
57 capv_idPr
58 capvv
59 cap0v
60 capv0
61 capfv
62 capvf
63 memv_cap
64 memv_capP
65 vspace_modl
66 vspace_modr
67 bigcapv_inf
68 subv_bigcapP
69 addv_complf
70 capv_compl
71 diffvSl
72 capv_diff
73 addv_diff_cap
74 addv_diff
75 dimv0
76 dimv_eq0
77 dimvf
78 dim_vline
79 dimvS
80 dimv_leqif_sup
81 dimv_leqif_eq
82 eqEdim
83 dimv_compl
84 dimv_cap_compl
85 dimv_sum_cap
86 dimv_disjoint_sum
87 dimv_add_leqif
88 diffv_eq0
89 dimv_leq_sum
90 directvE
91 directvP
92 directv_trivial
93 dimv_sum_leqif
94 directvEgeq
95 directv_addE
96 directv_addP
97 directv_add_unique
98 directv_sumE
99 directv_sum_independent
100 directv_sum_unique
101 memv_span
102 memv_span1
103 dim_span
104 span_subvP
105 sub_span
106 eq_span
107 span_def
108 span_nil
109 span_seq1
110 span_cons
111 span_cat
112 coord_span
113 nil_free
114 seq1_free
115 perm_free
116 free_directv
117 free_not0
118 freeP
119 coord_free
120 coord_sum_free
121 cat_free
122 catl_free
123 catr_free
124 filter_free
125 free_cons
126 freeE
127 freeNE
128 free_uniq
129 free_span
130 linear_of_free
131 span_basis
132 basis_free
133 coord_basis
134 nil_basis
135 seq1_basis
136 basis_not0
137 basis_mem
138 cat_basis
139 size_basis
140 basisEdim
141 perm_basis
142 vbasisP
143 vbasis_mem
144 coord_vbasis
145 span_bigcat
146 bigcat_free
147 bigcat_basis
148 lfunE
149 fun_of_lfunK
150 lfunP
151 lfun_addN
152 zero_lfunE
153 add_lfunE
154 opp_lfunE
155 sum_lfunE
156 scale_lfunE
157 id_lfunE
158 comp_lfunE
159 comp_lfunA
160 comp_lfun1l
161 comp_lfun1r
162 comp_lfun0l
163 comp_lfun0r
164 comp_lfunDl
165 comp_lfunDr
166 comp_lfunNl
167 comp_lfunNr
168 comp_lfunZl
169 comp_lfunZr
170 limgS
171 limg_line
172 limg0
173 memv_img
174 memv_imgP
175 lim0g
176 limg_add
177 limg_sum
178 limg_cap
179 limg_bigcap
180 limg_span
181 lfunPn
182 inv_lfun_def
183 limg_lfunVK
184 lkerE
185 memv_ker
186 limg_ker_compl
187 limg_ker_dim
188 limg_dim_eq
189 limg_basis_of
190 lker0P
191 limg_ker0
192 eq_limg_ker0
193 lker0_lfunK
194 lker0_compVf
195 lker0_limgf
196 lker0_lfunVK
197 lker0_compfV
198 lker0_compVKf
199 lker0_compKf
200 lker0_compfK
201 lker0_compfVK
202 lim1g
203 limg_comp
204 lpreim_cap_limg
205 lpreim0
206 lpreimS
207 lpreimK
208 memv_preim
209 memv_pi
210 memv_proj
211 memv_pi1
212 memv_pi2
213 daddv_pi_id
214 daddv_pi_proj
215 daddv_pi_add
216 projv_id
217 projv_proj
218 memv_projC
219 limg_proj
220 lker_proj
221 addv_pi1_proj
222 addv_pi2_id
223 addv_pi2_proj
224 addv_pi1_pi2
225 memv_sum_pi
226 sumv_pi_uniq_sum
227 sumv_pi_sum
228 sumv_pi_nat_sum
229 subvsP
230 subvs_inj
231 congr_subvs
232 vsval_is_linear
233 vsprojK
234 vsvalK
235 vsproj_is_linear
236 vsolve_eqP