blob: 1ba1f9ae1267c98031030687a409c210744483e6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
|
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
|
