A list of 195 redundant traits #1629
Description
With the help of Claude code, I gathered a list of (very likely) all redundant traits, i.e. Claude made a small addition to pi base web appending the list whenever the message on the website is triggered.
I checked 3 random outputs and it seems correct. All in all, these are about 8% of all manually added traits
It seems reasonable to remove (almost) all of these, at least thats we way we've been dealing with them recently.
However we should most definitely manually and carefully remove them. For example, if for properties A, B, C we know A => (B <=> C), I think (I could be mistaken, maybe this is taken care of by pi base web already) both B and C might be marked redundant, but removing them gives a loss of information.
Anyways, here is the list:
Found 195 redundant trait(s):
┌─────────┬───────────────────────────────────────────────────────────────────────────────────────┬──────────────────────────────────────────────┬─────────┬────────────┐
│ (index) │ space │ property │ spaceId │ propertyId │
├─────────┼───────────────────────────────────────────────────────────────────────────────────────┼──────────────────────────────────────────────┼─────────┼────────────┤
│ 0 │ 'Sierpinski space' │ 'Has multiple points' │ 10 │ 125 │
│ 1 │ 'Sierpinski space' │ 'Cardinality $\\geq 3$' │ 10 │ 175 │
│ 2 │ 'Sierpinski space' │ 'Hereditarily connected' │ 10 │ 196 │
│ 3 │ 'Sierpinski space' │ 'Has a generic point' │ 10 │ 201 │
│ 4 │ 'Either-Or Topology' │ 'Extremally disconnected' │ 14 │ 49 │
│ 5 │ 'Cofinite topology on $\\mathbb R$' │ 'Cardinality $=\\mathfrak c$' │ 16 │ 65 │
│ 6 │ 'Fort space on a countably infinite set' │ 'Countably infinite' │ 20 │ 181 │
│ 7 │ 'Weak topology on separable Hilbert space' │ '$T_2$' │ 21 │ 3 │
│ 8 │ 'Weak topology on separable Hilbert space' │ 'Completely regular' │ 21 │ 12 │
│ 9 │ 'Weak topology on separable Hilbert space' │ 'Weakly locally compact' │ 21 │ 23 │
│ 10 │ 'Weak topology on separable Hilbert space' │ 'Separable' │ 21 │ 26 │
│ 11 │ 'Weak topology on separable Hilbert space' │ 'Cardinality $=\\mathfrak c$' │ 21 │ 65 │
│ 12 │ 'Weak topology on separable Hilbert space' │ 'Indiscrete' │ 21 │ 129 │
│ 13 │ 'Euclidean real numbers $\\mathbb R$' │ 'Pseudocompact' │ 25 │ 22 │
│ 14 │ 'Euclidean real numbers $\\mathbb R$' │ 'Second countable' │ 25 │ 27 │
│ 15 │ 'Euclidean real numbers $\\mathbb R$' │ 'Metrizable' │ 25 │ 53 │
│ 16 │ 'Euclidean real numbers $\\mathbb R$' │ 'Cardinality $=\\mathfrak c$' │ 25 │ 65 │
│ 17 │ 'Irrational numbers $\\mathbb R\\setminus\\mathbb Q$' │ 'Pseudocompact' │ 28 │ 22 │
│ 18 │ 'Irrational numbers $\\mathbb R\\setminus\\mathbb Q$' │ 'Weakly locally compact' │ 28 │ 23 │
│ 19 │ 'Irrational numbers $\\mathbb R\\setminus\\mathbb Q$' │ 'Cardinality $=\\mathfrak c$' │ 28 │ 65 │
│ 20 │ 'Hilbert cube $[0,1]^\\omega$' │ 'Separable' │ 32 │ 26 │
│ 21 │ 'Hilbert cube $[0,1]^\\omega$' │ 'Injectively path connected' │ 32 │ 38 │
│ 22 │ 'Hilbert cube $[0,1]^\\omega$' │ 'Indiscrete' │ 32 │ 129 │
│ 23 │ 'Ordinal space $\\omega+\\omega$' │ 'Discrete' │ 33 │ 52 │
│ 24 │ 'Ordinal space $\\omega+\\omega$' │ 'Countable' │ 33 │ 57 │
│ 25 │ 'Overlapping interval topology' │ 'Hereditarily paracompact' │ 45 │ 216 │
│ 26 │ 'Countable sum of Sierpinski spaces' │ '$T_1$' │ 47 │ 2 │
│ 27 │ 'Countable sum of Sierpinski spaces' │ 'Ultraparacompact' │ 47 │ 146 │
│ 28 │ 'Cofinite topology on $\\omega$ extended by a non-open generic point' │ 'Biconnected' │ 48 │ 44 │
│ 29 │ '$\\mathbb Q$ extended by a focal point' │ 'Has a point with a unique neighborhood' │ 50 │ 202 │
│ 30 │ 'Khalimsky line' │ 'Countably infinite' │ 51 │ 181 │
│ 31 │ 'Double pointed reals' │ 'Regular' │ 54 │ 11 │
│ 32 │ 'Countable complement extension topology on the real numbers' │ 'First countable' │ 55 │ 28 │
│ 33 │ 'Countable complement extension topology on the real numbers' │ 'Cardinality $=\\mathfrak c$' │ 55 │ 65 │
│ 34 │ "Smirnov's deleted sequence topology" │ 'Locally connected' │ 56 │ 41 │
│ 35 │ 'Rational sequence topology' │ 'Cardinality $=\\mathfrak c$' │ 57 │ 65 │
│ 36 │ 'Rational sequence topology' │ 'Basically disconnected' │ 57 │ 85 │
│ 37 │ 'Rational sequence topology' │ 'Has a $\\sigma$-locally finite network' │ 57 │ 117 │
│ 38 │ 'Indiscrete irrational extension of $\\mathbb R$' │ 'Indiscrete' │ 59 │ 129 │
│ 39 │ 'Pointed irrational extension of $\\mathbb R$' │ '$\\sigma$-compact' │ 61 │ 17 │
│ 40 │ 'Pointed irrational extension of $\\mathbb R$' │ 'Locally connected' │ 61 │ 41 │
│ 41 │ 'Michael line' │ 'Cardinality $=\\mathfrak c$' │ 63 │ 65 │
│ 42 │ 'Rational extension of the plane' │ 'Countably paracompact' │ 64 │ 32 │
│ 43 │ 'Irrational slope topology' │ 'Semimetrizable' │ 67 │ 102 │
│ 44 │ 'Deleted diameter topology' │ 'Countably paracompact' │ 68 │ 32 │
│ 45 │ 'Irregular lattice topology' │ '$T_{2 \\frac{1}{2}}$' │ 71 │ 4 │
│ 46 │ 'Irregular lattice topology' │ 'Functionally Hausdorff' │ 71 │ 9 │
│ 47 │ 'Irregular lattice topology' │ 'Second countable' │ 71 │ 27 │
│ 48 │ 'Irregular lattice topology' │ 'Totally separated' │ 71 │ 48 │
│ 49 │ 'Irregular lattice topology' │ 'Extremally disconnected' │ 71 │ 49 │
│ 50 │ 'Irregular lattice topology' │ 'Countable' │ 71 │ 57 │
│ 51 │ 'Irregular lattice topology' │ 'Indiscrete' │ 71 │ 129 │
│ 52 │ 'Arens square' │ 'Scattered' │ 72 │ 51 │
│ 53 │ 'Simplified arens square' │ 'Sequentially compact' │ 73 │ 20 │
│ 54 │ 'Simplified arens square' │ 'Indiscrete' │ 73 │ 129 │
│ 55 │ 'Niemytzki plane' │ 'Has a $\\sigma$-locally finite network' │ 74 │ 117 │
│ 56 │ 'Niemytzki plane' │ 'Has a $\\sigma$-locally finite $k$-network' │ 74 │ 118 │
│ 57 │ 'Niemytzki plane' │ 'Realcompact' │ 74 │ 162 │
│ 58 │ 'Sorgenfrey plane' │ 'Pseudocompact' │ 76 │ 22 │
│ 59 │ 'Sorgenfrey plane' │ 'Extremally disconnected' │ 76 │ 49 │
│ 60 │ 'Sorgenfrey plane' │ 'Cardinality $=\\mathfrak c$' │ 76 │ 65 │
│ 61 │ "Michael's product topology" │ 'Indiscrete' │ 77 │ 129 │
│ 62 │ 'Tychonoff plank' │ 'Extremally disconnected' │ 78 │ 49 │
│ 63 │ "B. Scott's modified Arens square" │ 'Regular' │ 80 │ 11 │
│ 64 │ 'Alexandroff plank' │ '$T_{3 \\frac{1}{2}}$' │ 81 │ 6 │
│ 65 │ 'Alexandroff plank' │ 'Indiscrete' │ 81 │ 129 │
│ 66 │ 'Sum of continuum-many Right Ray Topology on the Reals' │ 'Connected' │ 82 │ 36 │
│ 67 │ 'Line with uncountably many origins' │ 'Countably paracompact' │ 85 │ 32 │
│ 68 │ 'Deleted Dieudonné plank' │ 'Extremally disconnected' │ 87 │ 49 │
│ 69 │ 'Deleted Tychonoff corkscrew' │ 'Functionally Hausdorff' │ 89 │ 9 │
│ 70 │ 'Deleted Tychonoff corkscrew' │ 'Weakly countably compact' │ 89 │ 21 │
│ 71 │ 'Deleted Tychonoff corkscrew' │ 'Zero dimensional' │ 89 │ 50 │
│ 72 │ "Hewitt's condensed corkscrew" │ 'Normal' │ 90 │ 13 │
│ 73 │ "Hewitt's condensed corkscrew" │ 'Compact' │ 90 │ 16 │
│ 74 │ "Hewitt's condensed corkscrew" │ 'Ultraconnected' │ 90 │ 40 │
│ 75 │ "Hewitt's condensed corkscrew" │ 'Indiscrete' │ 90 │ 129 │
│ 76 │ 'Thomas plank' │ 'Zero dimensional' │ 91 │ 50 │
│ 77 │ 'Strong parallel line topology' │ 'Regular' │ 94 │ 11 │
│ 78 │ 'Strong parallel line topology' │ 'Lindelöf' │ 94 │ 18 │
│ 79 │ 'Strong parallel line topology' │ 'Extremally disconnected' │ 94 │ 49 │
│ 80 │ 'Strong parallel line topology' │ 'Indiscrete' │ 94 │ 129 │
│ 81 │ 'Concentric circles' │ 'Perfectly normal' │ 95 │ 15 │
│ 82 │ 'Concentric circles' │ 'Sequentially compact' │ 95 │ 20 │
│ 83 │ 'Concentric circles' │ 'Separable' │ 95 │ 26 │
│ 84 │ 'Concentric circles' │ 'Second countable' │ 95 │ 27 │
│ 85 │ 'Concentric circles' │ 'Connected' │ 95 │ 36 │
│ 86 │ 'Concentric circles' │ 'Cardinality $=\\mathfrak c$' │ 95 │ 65 │
│ 87 │ 'Concentric circles' │ 'Indiscrete' │ 95 │ 129 │
│ 88 │ 'Appert space' │ 'Weakly locally compact' │ 96 │ 23 │
│ 89 │ 'Appert space' │ 'First countable' │ 96 │ 28 │
│ 90 │ 'Appert space' │ 'Indiscrete' │ 96 │ 129 │
│ 91 │ 'One-point compactification of the sequential fan $S_\\omega$' │ 'W-space' │ 97 │ 187 │
│ 92 │ 'Minimal Hausdorff topology' │ 'Indiscrete' │ 98 │ 129 │
│ 93 │ 'Continuum power of a countable discrete space' │ '$T_{3 \\frac{1}{2}}$' │ 101 │ 6 │
│ 94 │ 'Continuum power of a countable discrete space' │ 'Weakly locally compact' │ 101 │ 23 │
│ 95 │ 'Continuum power of a countable discrete space' │ 'Biconnected' │ 101 │ 44 │
│ 96 │ 'Continuum power of a countable discrete space' │ 'Scattered' │ 101 │ 51 │
│ 97 │ 'Baire space of weight continuum $B(\\mathfrak c)$' │ 'Countable chain condition' │ 102 │ 29 │
│ 98 │ 'Continuum power of $[0,1]$' │ 'Has countable spread' │ 103 │ 197 │
│ 99 │ 'Product of the first-uncountable ordinal with the continuum-power of unit intervals' │ 'Compact' │ 104 │ 16 │
│ 100 │ 'Product of the first-uncountable ordinal with the continuum-power of unit intervals' │ 'Meager' │ 104 │ 56 │
│ 101 │ 'Product of the first-uncountable ordinal with the continuum-power of unit intervals' │ 'Indiscrete' │ 104 │ 129 │
│ 102 │ 'Helly space' │ 'Cardinality $\\lt\\mathfrak c$' │ 105 │ 58 │
│ 103 │ 'Countable box product of reals' │ 'Pseudocompact' │ 107 │ 22 │
│ 104 │ 'Countable box product of reals' │ 'Weakly locally compact' │ 107 │ 23 │
│ 105 │ 'Countable box product of reals' │ 'Locally orderable' │ 107 │ 120 │
│ 106 │ 'Stone-Čech compactification $\\beta\\omega$ of the integers' │ 'Sequentially compact' │ 108 │ 20 │
│ 107 │ 'Stone-Čech compactification $\\beta\\omega$ of the integers' │ 'First countable' │ 108 │ 28 │
│ 108 │ 'Stone-Čech compactification $\\beta\\omega$ of the integers' │ 'Scattered' │ 108 │ 51 │
│ 109 │ 'Stone-Čech compactification $\\beta\\omega$ of the integers' │ 'Cardinality $\\leq 2^{\\mathfrak c}$' │ 108 │ 59 │
│ 110 │ 'Stone-Čech compactification $\\beta\\omega$ of the integers' │ 'Indiscrete' │ 108 │ 129 │
│ 111 │ 'Strong ultrafilter topology' │ 'Countably paracompact' │ 110 │ 32 │
│ 112 │ 'Strong ultrafilter topology' │ 'Anticompact' │ 110 │ 136 │
│ 113 │ 'Single ultrafilter subspace of $\\beta\\omega$' │ '$T_2$' │ 111 │ 3 │
│ 114 │ 'Single ultrafilter subspace of $\\beta\\omega$' │ 'Pseudocompact' │ 111 │ 22 │
│ 115 │ 'Single ultrafilter subspace of $\\beta\\omega$' │ 'Zero dimensional' │ 111 │ 50 │
│ 116 │ 'Single ultrafilter subspace of $\\beta\\omega$' │ 'Discrete' │ 111 │ 52 │
│ 117 │ 'Single ultrafilter subspace of $\\beta\\omega$' │ 'Anticompact' │ 111 │ 136 │
│ 118 │ "Closed Topologist's Sine Curve" │ 'Locally connected' │ 114 │ 41 │
│ 119 │ 'Integer broom' │ '$T_1$' │ 118 │ 2 │
│ 120 │ 'Integer broom' │ 'Compact' │ 118 │ 16 │
│ 121 │ 'Integer broom' │ 'Path connected' │ 118 │ 37 │
│ 122 │ 'Integer broom' │ 'Indiscrete' │ 118 │ 129 │
│ 123 │ 'Integer broom' │ 'Has a point with a unique neighborhood' │ 118 │ 202 │
│ 124 │ "Gustin's sequence space" │ 'First countable' │ 122 │ 28 │
│ 125 │ "Gustin's sequence space" │ 'Indiscrete' │ 122 │ 129 │
│ 126 │ "Roy's lattice space" │ 'Indiscrete' │ 123 │ 129 │
│ 127 │ "Roy's lattice subspace" │ 'Extremally disconnected' │ 124 │ 49 │
│ 128 │ "Roy's lattice subspace" │ 'Scattered' │ 124 │ 51 │
│ 129 │ "Roy's lattice subspace" │ 'Indiscrete' │ 124 │ 129 │
│ 130 │ 'Knaster-Kuratowski fan' │ 'Pseudocompact' │ 125 │ 22 │
│ 131 │ 'Knaster-Kuratowski fan' │ 'Cardinality $=\\mathfrak c$' │ 125 │ 65 │
│ 132 │ 'Knaster-Kuratowski fan' │ 'Indiscrete' │ 125 │ 129 │
│ 133 │ 'Punctured Knaster-Kuratowski fan' │ 'Compact' │ 126 │ 16 │
│ 134 │ 'Punctured Knaster-Kuratowski fan' │ 'Cardinality $=\\mathfrak c$' │ 126 │ 65 │
│ 135 │ "Miller's biconnected set" │ 'Countable chain condition' │ 128 │ 29 │
│ 136 │ "Tangora's connected space" │ 'Indiscrete' │ 130 │ 129 │
│ 137 │ 'Real line with post office metric' │ 'Countable chain condition' │ 133 │ 29 │
│ 138 │ 'Real line with post office metric' │ 'Zero dimensional' │ 133 │ 50 │
│ 139 │ 'Real line with post office metric' │ 'Scattered' │ 133 │ 51 │
│ 140 │ 'Real line with post office metric' │ 'Cardinality $=\\mathfrak c$' │ 133 │ 65 │
│ 141 │ 'Radial metric on the plane' │ 'Cardinality $=\\mathfrak c$' │ 134 │ 65 │
│ 142 │ "Bing's Example G" │ 'Perfectly normal' │ 136 │ 15 │
│ 143 │ "Bing's Example G" │ 'Countably compact' │ 136 │ 19 │
│ 144 │ "Michael's subspace of Bing's Example G" │ 'Countably paracompact' │ 137 │ 32 │
│ 145 │ "Michael's subspace of Bing's Example G" │ 'Indiscrete' │ 137 │ 129 │
│ 146 │ 'Real numbers extended by a point with co-countable open neighborhoods' │ 'Hereditarily Lindelöf' │ 140 │ 131 │
│ 147 │ 'Real numbers extended by a point with co-countable open neighborhoods' │ 'Hereditarily separable' │ 140 │ 180 │
│ 148 │ 'Butterfly space' │ 'Weakly locally compact' │ 143 │ 23 │
│ 149 │ 'Diamond poset $2\\times 2$ with Alexandrov topology' │ 'Door' │ 144 │ 126 │
│ 150 │ 'Free ultrafilter topology on $\\omega$' │ '$T_1$' │ 145 │ 2 │
│ 151 │ 'Free ultrafilter topology on $\\omega$' │ 'Hyperconnected' │ 145 │ 39 │
│ 152 │ 'Two-sided long line' │ 'Perfectly normal' │ 149 │ 15 │
│ 153 │ 'Right "open-ray" topology on $[0,1]\\cap\\mathbb Q$' │ 'Alexandrov' │ 151 │ 90 │
│ 154 │ 'Open long ray' │ 'Perfectly normal' │ 153 │ 15 │
│ 155 │ 'Open long ray' │ 'Homogeneous' │ 153 │ 86 │
│ 156 │ 'Arens space' │ 'Countable' │ 156 │ 57 │
│ 157 │ 'Sum of singleton and two-point indiscrete space' │ 'Partition topology' │ 164 │ 185 │
│ 158 │ 'Sphere $S^2$' │ 'Homogeneous' │ 169 │ 86 │
│ 159 │ 'Sphere $S^2$' │ 'Empty' │ 169 │ 137 │
│ 160 │ 'Sphere $S^2$' │ 'Embeddable into Euclidean space' │ 169 │ 184 │
│ 161 │ 'Sphere $S^2$' │ 'Contractible' │ 169 │ 199 │
│ 162 │ 'Circle $S^1$' │ '$T_2$' │ 170 │ 3 │
│ 163 │ 'Circle $S^1$' │ 'Cardinality $=\\mathfrak c$' │ 170 │ 65 │
│ 164 │ 'Circle $S^1$' │ 'Has a cut point' │ 170 │ 204 │
│ 165 │ 'Radial plane' │ 'Cardinality $=\\mathfrak c$' │ 175 │ 65 │
│ 166 │ 'Euclidean Plane $\\mathbb R^2$' │ 'Pseudocompact' │ 176 │ 22 │
│ 167 │ 'Euclidean Plane $\\mathbb R^2$' │ 'Second countable' │ 176 │ 27 │
│ 168 │ 'Euclidean Plane $\\mathbb R^2$' │ 'Metrizable' │ 176 │ 53 │
│ 169 │ 'Euclidean Plane $\\mathbb R^2$' │ 'Embeddable in $\\mathbb R$' │ 176 │ 97 │
│ 170 │ 'Euclidean Plane $\\mathbb R^2$' │ 'Has a cut point' │ 176 │ 204 │
│ 171 │ "Misra's subspace of $E_0$" │ '$T_{2 \\frac{1}{2}}$' │ 178 │ 4 │
│ 172 │ 'Disjoint union of continuum many copies of $\\mathbb{Q}$' │ 'Cardinality $=\\mathfrak c$' │ 182 │ 65 │
│ 173 │ 'One-point compactification of the metric fan' │ 'Totally disconnected' │ 185 │ 47 │
│ 174 │ 'Converging sequence of non-Hausdorff spaces' │ 'W-space' │ 186 │ 187 │
│ 175 │ 'Right ray topology on a three-point set' │ 'Has a dispersion point' │ 187 │ 45 │
│ 176 │ 'Right ray topology on a three-point set' │ 'Door' │ 187 │ 126 │
│ 177 │ 'Right ray topology on a three-point set' │ 'Cardinality $\\geq 3$' │ 187 │ 175 │
│ 178 │ 'Sum of singleton and Sierpinski space' │ 'Connected' │ 188 │ 36 │
│ 179 │ 'Dieudonné plank' │ 'Pseudocompact' │ 191 │ 22 │
│ 180 │ 'Dieudonné plank' │ 'Extremally disconnected' │ 191 │ 49 │
│ 181 │ 'Modified telophase topology' │ 'Cardinality $=\\mathfrak c$' │ 192 │ 65 │
│ 182 │ 'Modified telophase topology' │ 'US' │ 192 │ 99 │
│ 183 │ 'Long circle' │ 'Locally connected' │ 196 │ 41 │
│ 184 │ 'Disjoint union of the reals and a singleton' │ 'Compact' │ 198 │ 16 │
│ 185 │ 'Infinite earring' │ 'Locally Euclidean' │ 201 │ 122 │
│ 186 │ 'Metric fan with $\\omega$-many spines' │ 'Countably infinite' │ 202 │ 181 │
│ 187 │ 'Three-point set with the basis $\\{\\{0\\},X\\}$' │ '$T_0$' │ 203 │ 1 │
│ 188 │ 'Three-point set with the basis $\\{\\{0\\},X\\}$' │ 'Semiregular' │ 203 │ 10 │
│ 189 │ 'Three-point set with the basis $\\{\\{0,1\\},X\\}$' │ '$T_0$' │ 204 │ 1 │
│ 190 │ 'Three-point set with the basis $\\{\\{0,1\\},X\\}$' │ 'Semiregular' │ 204 │ 10 │
│ 191 │ 'Pseudocircle' │ 'Normal' │ 213 │ 13 │
│ 192 │ 'Lexicographically ordered $\\mathbb Z^{\\omega_1}$' │ 'Cardinality $\\lt\\mathfrak c$' │ 214 │ 58 │
│ 193 │ "Katětov's non-normal subspace of $\\beta\\mathbb{N}$" │ 'Cardinality $=\\mathfrak c$' │ 216 │ 65 │
│ 194 │ 'Product topology on $\\omega^{2^\\mathfrak{c}}$' │ 'Has countable spread' │ 1103 │ 197 │