-
Notifications
You must be signed in to change notification settings - Fork 3
/
BIG_FILES
118 lines (110 loc) · 2.62 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
### hol
# files > 10 M
DIMINDEX_HAS_SIZE_FINITE_DIFF
INVOLUTION_EVEN_NOFIXPOINTS
ITERATE_REFLECT
REAL_SGN_EQ_INEQ
REAL_SHRINK_LT
REAL_SUB_POLYFUN_ALT
REAL_SUB_POW
TOPOLOGICAL_SORT
### Multivariate
URYSOHN_LEMMA
CHAIN_BOUNDARY_BOUNDARY
GRASSMANN_PLUCKER_4
HOMOTOPIC_IMP_HOMOLOGOUS_REL_CHAIN_MAPS
# files > 10M
ALEXANDER_SUBBASE_THEOREM
BACK_AND_FORTH
BAIRE_EQ_FSIGMA_PREIMAGE_OPEN_GEN
BILINEAR_VSUM_CONVOLUTION_2
BORSUK_ODD_MAPPING_DEGREE_STEP
CARD_EXP_ADD
CARD_GE_PERFECT_SET
CARD_LE_CONNECTED_COMPONENTS_ALT
CARD_SQUARE_INFINITE
CAUCHY_CONTINUOUS_MAP_EXTENDS_TO_CONTINUOUS_CLOSURE_OF
CLOSED_INTERVAL_DROPOUT
COMPLETE_HAUSDIST_UNIV
CONNECTED_SPACE_PRODUCT_TOPOLOGY
COUNTABLE_NONCONTINUOUS_RIGHT_LIMITS
DET_OPEN_MAP
EFFECTIVELY_COUNTABLE_CLOPEN_IN_CHAIN_UNIONS
EQ_PRIME_EXP
EULER_ROTATION_THEOREM
EULER_ROTOINVERSION_THEOREM
EXACT_SEQUENCE_HEXAGON_LEMMA
FINITELY_GENERATED_ABELIAN_SUBGROUP_EXPLICIT
FINITELY_GENERATED_ABELIAN_SUBGROUP_STRUCTURE_ISOMORPHISM
FOUR_LEMMA_EPI
FOUR_LEMMA_MONO
GDELTA_HOMEOMORPHIC_SPACE_CLOSED_IN_PRODUCT
GRASSMANN_PLUCKER_3
GROUP_IMAGE_REDUCED_HOMOLOGY_GROUP
HADAMARD_INEQUALITY_ROW
HOMOEOMORPHISM_PASTE
HOMOLOGY_ADDITIVITY_AXIOM_GEN
INVARIANCE_OF_DOMAIN_EUCLIDEAN_SPACE
IS_INTERVAL_PCROSS
IS_INTERVAL_SUMS
ISOMORPHIC_RELATIVE_HOMOLOGY_GROUPS_EUCLIDEAN_COMPLEMENTS
KURATOWSKI_COMPONENT_NUMBER_INVARIANCE
LIM_BILINEAR_CONVOLUTION
LIPSCHITZ_CONTINUOUS_MAP_METRIC
LOCALLY_CONNECTED_NOT_COUNTABLE_CLOSED_UNION
MAX_LE_LCM_EQ
METRIC_BAIRE_CATEGORY
MUMFORD_LEMMA
ORDER_EXISTENCE_CARD
PERMUTES_COMPOSE
REAL_NON_MONOTONE
RELATIVE_HOMOLOGY_GROUP_EUCLIDEAN_COMPLEMENT_STEP
RIGHT_POLAR_DECOMPOSITION
SEPARATION_BY_CLOSED_INTERMEDIATES_EQ_COUNT
SINGULAR_FACE_ORIENTED_SIMPLEX
STRICTLY_INCREASING_ALT
SUBSET_REAL_INTERVAL
SUM_OVER_PERMUTATIONS_INSERT
SUSLIN_SUSLIN
thm43768123
thm58632923
thm74401368
thm74488330
thm74575354
thm74652437
TOSET_COFINAL_WOSET
# files > 7 M
BROUWER_DEGREE2_REFLECTION
BROUWER_REDUCTION_THEOREM_GEN
CAUCHY_CONTINUOUS_MAP_ON_INTERMEDIATE_CLOSURE
CHARACTERISTIC_POLYNOMIAL
CLOSED_LOCAL_HOMEOMORPHISM_IMP_PROPER_GEN
COLLINEAR_1
COLLINEAR_3_2D
CONNECTED_CHAIN
DET_4
DISJOINT_INTERVAL
DOT_DROPOUT
DOT_VECTORIZE
EVENPERM_CYCLIC
GCD_MUL_COPRIME
GROUP_ISOMORPHISM_RELATIVE_HOMOLOGY_GROUP_UPPER_HEMISPHERE
HAUSDIST_BALLS
HOMOTOPIC_IMP_HOMOLOGOUS_REL_CHAIN_MAPS
ITERATO_EQ
LAVRENTIEV_HOMEOMORPHISM
MONOTONE_MAP_INTO_EUCLIDEANREAL_ALT
NORMAL_SPACE_FSIGMAS
OEP
REAL_SGNS_EQ
RECURSION_CASEWISE
RECURSION_ON_DYADIC_FRACTIONS
SCHREIER_TRANSVERSAL_LEMMA
SINGULAR_BOUNDARY_EQ_CYCLE_SING
STRICTLY_DECREASING_ALT
SUFFICIENT_ITERATED_SINGULAR_SUBDIVISION_EXISTS
thm1482678
thm87252427
thm87567155
TIETZE_EXTENSION_CLOSED_REAL_INTERVAL
WF_REC_TAIL_GENERAL