-
Notifications
You must be signed in to change notification settings - Fork 4
/
Copy pathBIG_FILES
262 lines (262 loc) · 7.19 KB
/
BIG_FILES
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
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
ABSOLUTE_INTEGRATION_BY_PARTS
ABSOLUTELY_CONTINUOUS_MEASURE_IMAGE
ABSOLUTELY_CONTINUOUS_ON_BILINEAR
ABSOLUTELY_CONTINUOUS_ON_INTERIOR
ABSOLUTELY_INTEGRABLE_APPROXIMATE_CONTINUOUS
ABSOLUTELY_INTEGRABLE_IMPROPER
ABSOLUTELY_INTEGRABLE_SET_VARIATION
ABSOLUTELY_SETCONTINUOUS_ON_IMP_HAS_BOUNDED_SETVARIATION_ON
ACCESSIBLE_FRONTIER_ANR_INTER_COMPLEMENT_COMPONENT
ALEXANDER_SUBBASE_THEOREM
ANR_OPEN_UNIONS
ANR_UNION_EXTENSION_LEMMA
APPELL_SEQUENCE
AR_CLOSED_UNION_LOCAL
BABY_SARD
BACK_AND_FORTH
BAIRE_EQ_FSIGMA_PREIMAGE_OPEN_GEN
BANACH_SPROPERTY_IMP_FINITE_PREIMAGES
BERNOULLI_EVEN_BOUND
BICONNECTED_IMP_CONTINUOUS_ON
BILINEAR_VSUM_CONVOLUTION_2
BINOM_MUL_SHIFT
BORSUK_HOMOTOPY_EXTENSION_HOMOTOPIC
BORSUKIAN_IMP_UNICOHERENT
BORSUK_ODD_MAPPING_DEGREE_STEP
BORSUK_ODD_MAPPING_GEN
BOUNDED_EQUIINTEGRAL_OVER_THIN_TAGGED_PARTIAL_DIVISION
BOUNDED_SETVARIATION_ABSOLUTELY_INTEGRABLE
BOUNDED_SETVARIATION_ABSOLUTELY_INTEGRABLE_INTERVAL
BROUWER_DEGREE1_HOMOTOPIC
BROUWER_DEGREE2_REFLECTION
CARATHEODORY_CONFORMAL_EXTENSION_LEMMA
CARD_EQ_COMPONENTS_IN_COMPACTIFICATION
CARD_EQ_FUNDAMENTAL_GROUP_COVERING_SPACE_ALT
CARD_EXP_ADD
CARD_GE_PERFECT_SET
CARD_LE_CONNECTED_COMPONENTS_ALT
CARD_SQUARE_INFINITE
CAUCHY_CONTINUOUS_MAP_EXTENDS_TO_CONTINUOUS_CLOSURE_OF
CAUCHY_INTEGRAL_FORMULA_GLOBAL
CAUCHY_THEOREM_HOMOTOPIC_LOOPS
CAUCHY_THEOREM_HOMOTOPIC_PATHS
CAUCHY_THEOREM_TRIANGLE_INTERIOR
CHAIN_BOUNDARY_BOUNDARY
CLOSED_INTERVAL_DROPOUT
CLOSED_LOCAL_HOMEOMORPHISM_IMP_PROPER_GEN
COMPLETE_HAUSDIST_UNIV
COMPLEX_SUB_POLYFUN_ALT
COMPLEX_SUB_POW
COMPONENT_INTERMEDIATE_CLOPEN
CONNECTED_CHAIN
CONNECTED_COMPONENT_EQ_WELLCHAINED
CONNECTED_INTER_DISJOINT_OPEN_FRONTIERS
CONNECTED_JACOBIAN_GRAPH
CONNECTED_JACOBIAN_RANGE_ALT
CONNECTED_SPACE_PRODUCT_TOPOLOGY
CONTINUOUS_BV_IMP_UNIFORMLY_CONTINUOUS
CONTINUOUS_MEASURE_DIFFERENTIABLE_IMAGE_TRANSLATION
COUNTABLE_NONCONTINUOUS_RIGHT_LIMITS
COVERING_LEMMA
COVERING_SPACE_CLOSED_MAP
COVERING_SPACE_FINITE_SHEETS_EQ_CLOSED_MAP_STRONG
COVERING_SPACE_LIFT_GENERAL
COVERING_SPACE_LIFT_HOMOTOPIC_PATHS
COVERING_SPACE_LIFT_HOMOTOPY
COVERING_SPACE_LOCALLY_HOMEOMORPHIC
COVERING_SPACE_LOCALLY_HOMEOMORPHIC_EQ
CTAN_CATN
DET_OPEN_MAP
DIMENSION_EQ_AFF_DIM
DIMINDEX_HAS_SIZE_FINITE_DIFF
DIVISION_DISJOINT_UNION
DIVISION_POINTS_SUBSET
DOMINATED_CONVERGENCE
DUGUNDJI
EFFECTIVELY_COUNTABLE_CLOPEN_IN_CHAIN_UNIONS
EQ_PRIME_EXP
EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_LE
EQUIINTEGRABLE_ON_SPLIT
EULER_ROTATION_THEOREM
EULER_ROTOINVERSION_THEOREM
EXACT_SEQUENCE_HEXAGON_LEMMA
EXISTS_DOUBLE_ARC_EXPLICIT
EXTEND_MAP_AFFINE_TO_SPHERE_COFINITE_GEN
EXTEND_MAP_AFFINE_TO_SPHERE_COFINITE_SIMPLE
EXTEND_MAP_SPHERE_TO_SPHERE_COFINITE_GEN
FACE_OF_CONVEX_HULL_INSERT_EQ
FACE_OF_POLYHEDRON_EXPLICIT
FACET_OF_POLYHEDRON_EXPLICIT
FACETS_OF_POLYHEDRON_EXPLICIT_DISTINCT
FASHODA_INTERLACE
FINITE_ANR_COMPLEMENT_COMPONENTS_CONCENTRIC
FINITELY_GENERATED_ABELIAN_SUBGROUP_EXPLICIT
FINITELY_GENERATED_ABELIAN_SUBGROUP_STRUCTURE_ISOMORPHISM
FOUR_LEMMA_EPI
FOUR_LEMMA_MONO
FUBINI_CLOSED_INTERVAL
FUBINI_INTEGRAL_SWAP
FUBINI_MEASURE
FUBINI_SIMPLE_LEMMA
FUNDAMENTAL_THEOREM_OF_CALCULUS_BARTLE
FUNDAMENTAL_THEOREM_OF_CALCULUS_STRONG
GDELTA_HOMEOMORPHIC_SPACE_CLOSED_IN_PRODUCT
GRASSMANN_PLUCKER_3
GRASSMANN_PLUCKER_4
GROUP_IMAGE_REDUCED_HOMOLOGY_GROUP
HADAMARD_INEQUALITY_ROW
HADAMARD_THREE_LINE_EXPLICIT_RE
HAS_ABSOLUTE_INTEGRAL_CHANGE_OF_VARIABLES
HAS_ABSOLUTE_INTEGRAL_CHANGE_OF_VARIABLES_INVERTIBLE
HAS_BOUNDED_VARIATION_ON_COMBINE_GEN
HAS_BOUNDED_VARIATION_ON_INTERIOR
HAS_COMPLEX_DERIVATIVE_CATN
HAS_INTEGRAL_NEGLIGIBLE
HAS_INTEGRAL_PASTECART_SYM_ALT
HAS_INTEGRAL_SPLIT
HAS_INTEGRAL_TWIDDLE
HAS_MEASURE_LINEAR_IMAGE
HAS_MEASURE_LINEAR_SUFFICIENT
HAS_MEASURE_SHEAR_INTERVAL
HAS_SIZE_INTER_SPHERE_1
HELLY_SELECTION_INCREASING
HENSTOCK_LEMMA_PART1
HOLOMORPHIC_ON_PASTE_ACROSS_LINE
HOLOMORPHIC_POWER_SERIES
HOMEOMORPHIC_MONOTONE_IMAGE_INTERVAL
HOMEOMORPHISM_GROUPING_POINTS_EXISTS
HOMEOMORPHISM_GROUPING_POINTS_EXISTS_GEN
HOMEOMORPHISM_MOVING_DENSE_COUNTABLE_SUBSETS_EXISTS
HOMEOMORPHISM_MOVING_POINT_EXISTS
HOMOEOMORPHISM_PASTE
HOMOLOGY_ADDITIVITY_AXIOM_GEN
HOMOTOPIC_IMP_HOMOLOGOUS_REL_CHAIN_MAPS
HOMOTOPY_EQUIVALENT_SEPARATION_SPHERE
HURWITZ_NO_ZEROS
INCREASING_LEFT_LIMIT_1
INDUCT_LINEAR_ELEMENTARY
INDUCT_MATRIX_ELEMENTARY
INDUCT_MATRIX_ROW_OPERATIONS
INESSENTIAL_NEIGHBOURHOOD_EXTENSION_LOGARITHM
INTEGRABLE_CCONTINUOUS_EXPLICIT
INTEGRABLE_CCONTINUOUS_EXPLICIT_SYMMETRIC
INTER_SPHERE_EQ_EMPTY
INVARIANCE_OF_DOMAIN_EUCLIDEAN_SPACE
INVARIANCE_OF_DOMAIN_SPHERE_AFFINE_SET_GEN
INVERSE_FUNCTION_THEOREM
INVERSE_FUNCTION_THEOREM_SUBSPACE
INVERSE_LIPSCHITZ_CONVEX_SPHERICAL_PROJECTION_EXPLICIT
INVOLUTION_EVEN_NOFIXPOINTS
IS_INTERVAL_CLOSURE
IS_INTERVAL_PCROSS
IS_INTERVAL_SUMS
ISOMORPHIC_RELATIVE_HOMOLOGY_GROUPS_EUCLIDEAN_COMPLEMENTS
ITERATE_REFLECT
JACOBIAN_SIGN_INVARIANCE
JORDAN_SCHOENFLIES
JORDAN_SCHOENFLIES_S2
KIRSZBRAUN
KURATOWSKI_COMPONENT_NUMBER_INVARIANCE
LAVRENTIEV_HOMEOMORPHISM
LEBESGUE_DIFFERENTIATION_THEOREM_COMPACT
LEBESGUE_MEASURABLE_POINTS_OF_DIFFERENTIABILITY_WITHIN
LHOSPITAL
LIM_BILINEAR_CONVOLUTION
LIPSCHITZ_CONTINUOUS_MAP_METRIC
LOCALLY_COMPACT_CONNECTED_IMP_PATH_CONNECTED
LOCALLY_CONNECTED_FRONTIER_ANR
LOCALLY_CONNECTED_NOT_COUNTABLE_CLOSED_UNION
LOCALLY_FCCOVERABLE
LOCALLY_FCCOVERABLE_ALT
LOCALLY_LIPSCHITZ_GEN
LOG2_APPROX_32
LUZIN_NPROPERTY_IMP_COUNTABLE_PREIMAGES
MAX_LE_LCM_EQ
MEASURABLE_MIDPOINT_CONVEX_IMP_CONVEX_GEN
MEASURABLE_ON_PARTIAL_DERIVATIVES
MEASURABLE_OUTER_INTERVALS_BOUNDED
MEASURE_DIFFERENTIABLE_IMAGE_APPROX_GEN
METRIC_BAIRE_CATEGORY
MONODROMY_CONTINUOUS_LOG
MONOTONE_CONNECTED_PREIMAGES_IMP_PROPER_MAP
MONOTONE_CONVERGENCE_INTERVAL
MONTEL
MUMFORD_LEMMA
NEGLIGIBLE_IMAGE_INDEFINITE_INTEGRAL
NEGLIGIBLE_LOCALLY_LIPSCHITZ_IMAGE
ODD_MAP_HOMOTOPY_LEMMA
OPEN_MAPPING_THM
OPERATIVE_ABSOLUTELY_SETCONTINUOUS_ON
OPERATIVE_DIVISION
ORDER_EXISTENCE_CARD
PARTIAL_DIVISION_EXTEND_1
PATH_CONTAINS_ARC
PERMUTES_COMPOSE
PI_APPROX_32
POLYHEDRON_EQ_FINITE_EXPOSED_FACES
POLYHEDRON_RIDGE_TWO_FACETS
PROPER_LOCAL_HOMEOMORPHISM_IMP_COVERING_MAP
RADEMACHER_UNIV
REAL_EULER_MACLAURIN
REAL_NON_MONOTONE
REAL_SGN_EQ_INEQ
REAL_SHRINK_LT
REAL_SUB_POLYFUN_ALT
REAL_SUB_POW
RELATIVE_HOMOLOGY_GROUP_EUCLIDEAN_COMPLEMENT_STEP
RIGHT_POLAR_DECOMPOSITION
ROTATION_TO_GENERAL_POSITION_EXISTS_GEN
SCHOTTKY
SECOND_MEAN_VALUE_THEOREM_FULL
SEMI_LOCALLY_CONNECTED
SEPARATION_BY_CLOSED_INTERMEDIATES_EQ_COUNT
SIMPLE_CLOSED_PATH_WINDING_NUMBER_INSIDE
SIMPLE_PATH_JOIN_IMP
SIMPLE_PATH_LENGTH_MINIMAL
SIMPLE_PATH_PARTCIRCLEPATH
SIMPLE_PATH_REVERSEPATH
SIMPLE_PATH_SHIFTPATH
SIMPLE_PATH_SUBPATH
SIMPLICIAL_SUBDIVISION_OF_CELL_COMPLEX_LOWDIM
SIMPLY_CONNECTED_UNION
SINGULAR_FACE_ORIENTED_SIMPLEX
SPLIT_INSIDE_SIMPLE_CLOSED_CURVE
STARLIKE_COMPACT_PROJECTIVE
STEPANOV_GEN
STONE_WEIERSTRASS_ALT
STRICTLY_INCREASING_ALT
SUBSET_REAL_INTERVAL
SUM_CONTENT_AREA_OVER_THIN_DIVISION
SUM_OVER_PERMUTATIONS_INSERT
SUSLIN_SUSLIN
THETA_CURVE_INSIDE_CASES
thm111001424
thm116809061
thm158037215
thm173384404
thm173566180
thm179700212
thm188066193
thm197746085
thm198522663
thm205376205
thm213609960
thm214478351
thm214825502
thm44211857
thm58915147
thm74606197
thm74693159
thm74780183
thm74857266
TOPOLOGICAL_SORT
TORHORST_CONFORMAL_EXTENSION_THEOREM
TOSET_COFINAL_WOSET
UNIVERSAL_COVERING_SPACE
URYSOHN_LEMMA
VECTOR_VARIATION_CONTINUOUS_LEFT
VECTOR_VARIATION_CONTINUOUS_RIGHT
VITALI_COVERING_LEMMA_CBALLS_BALLS
VITALI_COVERING_THEOREM_CBALLS
WEAK_LEBESGUE_POINTS_IMP_IVT
WINDING_NUMBER_AHLFORS_LEMMA