From 14eab6b5522032cd4421a28654587a91b0f32f68 Mon Sep 17 00:00:00 2001 From: danflapjax <12000932+danflapjax@users.noreply.github.com> Date: Sat, 12 Oct 2024 10:37:52 -0700 Subject: [PATCH 01/13] add property, theorems, and traits --- properties/P000196.md | 11 +++++++++++ spaces/S000187/properties/P000196.md | 7 +++++++ spaces/S000199/properties/P000002.md | 7 ------- spaces/S000199/properties/P000014.md | 10 ---------- spaces/S000199/properties/P000039.md | 9 --------- spaces/S000199/properties/P000086.md | 7 ------- spaces/S000199/properties/P000139.md | 7 +++++++ .../P000039.md => S000199/properties/P000181.md} | 4 ++-- spaces/S000199/properties/P000196.md | 7 +++++++ spaces/S000200/properties/P000002.md | 7 ------- spaces/S000200/properties/P000014.md | 10 ---------- spaces/S000200/properties/P000016.md | 7 +++++++ spaces/S000200/properties/P000039.md | 9 --------- spaces/S000200/properties/P000086.md | 8 -------- .../P000040.md => S000200/properties/P000181.md} | 4 ++-- spaces/S000200/properties/P000196.md | 7 +++++++ theorems/T000546.md | 9 +++++++++ theorems/T000547.md | 9 +++++++++ theorems/T000548.md | 11 +++++++++++ theorems/T000549.md | 9 +++++++++ theorems/T000550.md | 11 +++++++++++ theorems/T000551.md | 12 ++++++++++++ theorems/T000552.md | 12 ++++++++++++ 23 files changed, 123 insertions(+), 71 deletions(-) create mode 100644 properties/P000196.md create mode 100644 spaces/S000187/properties/P000196.md delete mode 100644 spaces/S000199/properties/P000002.md delete mode 100644 spaces/S000199/properties/P000014.md delete mode 100644 spaces/S000199/properties/P000039.md delete mode 100644 spaces/S000199/properties/P000086.md create mode 100644 spaces/S000199/properties/P000139.md rename spaces/{S000187/properties/P000039.md => S000199/properties/P000181.md} (52%) create mode 100644 spaces/S000199/properties/P000196.md delete mode 100644 spaces/S000200/properties/P000002.md delete mode 100644 spaces/S000200/properties/P000014.md create mode 100644 spaces/S000200/properties/P000016.md delete mode 100644 spaces/S000200/properties/P000039.md delete mode 100644 spaces/S000200/properties/P000086.md rename spaces/{S000187/properties/P000040.md => S000200/properties/P000181.md} (52%) create mode 100644 spaces/S000200/properties/P000196.md create mode 100644 theorems/T000546.md create mode 100644 theorems/T000547.md create mode 100644 theorems/T000548.md create mode 100644 theorems/T000549.md create mode 100644 theorems/T000550.md create mode 100644 theorems/T000551.md create mode 100644 theorems/T000552.md diff --git a/properties/P000196.md b/properties/P000196.md new file mode 100644 index 000000000..01f89ee37 --- /dev/null +++ b/properties/P000196.md @@ -0,0 +1,11 @@ +--- +uid: P000196 +name: Hereditarily connected +aliases: +- Totally ordered topology +refs: +- zb: "0396.54009" + name: On ultrapseudocompact and related spaces (T. Nieminen) +--- + +. diff --git a/spaces/S000187/properties/P000196.md b/spaces/S000187/properties/P000196.md new file mode 100644 index 000000000..e29f17433 --- /dev/null +++ b/spaces/S000187/properties/P000196.md @@ -0,0 +1,7 @@ +--- +space: S000187 +property: P000196 +value: true +--- + +By construction. diff --git a/spaces/S000199/properties/P000002.md b/spaces/S000199/properties/P000002.md deleted file mode 100644 index e7a65eb1b..000000000 --- a/spaces/S000199/properties/P000002.md +++ /dev/null @@ -1,7 +0,0 @@ ---- -space: S000199 -property: P000002 -value: false ---- - -Every neighborhood of $1$ is a neighborhood of $0$. diff --git a/spaces/S000199/properties/P000014.md b/spaces/S000199/properties/P000014.md deleted file mode 100644 index 4d96693a4..000000000 --- a/spaces/S000199/properties/P000014.md +++ /dev/null @@ -1,10 +0,0 @@ ---- -space: S000199 -property: P000014 -value: true ---- - -The collection of closed sets is a chain under inclusion; -that is, -for each pair of closed sets, one is contained in the other. -Therefore every subspace is vacuously {P13}. diff --git a/spaces/S000199/properties/P000039.md b/spaces/S000199/properties/P000039.md deleted file mode 100644 index 7edff5528..000000000 --- a/spaces/S000199/properties/P000039.md +++ /dev/null @@ -1,9 +0,0 @@ ---- -space: S000199 -property: P000039 -value: true ---- - -The topology is a chain under inclusion; -that is, -for each pair of open sets, one is contained in the other. diff --git a/spaces/S000199/properties/P000086.md b/spaces/S000199/properties/P000086.md deleted file mode 100644 index 557402636..000000000 --- a/spaces/S000199/properties/P000086.md +++ /dev/null @@ -1,7 +0,0 @@ ---- -space: S000199 -property: P000086 -value: false ---- - -$0$ belongs to every nonempty open set, but $1$ does not belong to $(\leftarrow,0]$. diff --git a/spaces/S000199/properties/P000139.md b/spaces/S000199/properties/P000139.md new file mode 100644 index 000000000..aede17d35 --- /dev/null +++ b/spaces/S000199/properties/P000139.md @@ -0,0 +1,7 @@ +--- +space: S000199 +property: P000139 +value: true +--- + +$\{0\}$ is open. diff --git a/spaces/S000187/properties/P000039.md b/spaces/S000199/properties/P000181.md similarity index 52% rename from spaces/S000187/properties/P000039.md rename to spaces/S000199/properties/P000181.md index 7d239f6d7..21e3c555e 100644 --- a/spaces/S000187/properties/P000039.md +++ b/spaces/S000199/properties/P000181.md @@ -1,6 +1,6 @@ --- -space: S000187 -property: P000039 +space: S000199 +property: P000181 value: true --- diff --git a/spaces/S000199/properties/P000196.md b/spaces/S000199/properties/P000196.md new file mode 100644 index 000000000..cc091bd9f --- /dev/null +++ b/spaces/S000199/properties/P000196.md @@ -0,0 +1,7 @@ +--- +space: S000199 +property: P000196 +value: true +--- + +By construction. diff --git a/spaces/S000200/properties/P000002.md b/spaces/S000200/properties/P000002.md deleted file mode 100644 index ea4e1784b..000000000 --- a/spaces/S000200/properties/P000002.md +++ /dev/null @@ -1,7 +0,0 @@ ---- -space: S000200 -property: P000002 -value: false ---- - -Every neighborhood of $0$ is a neighborhood of $1$. diff --git a/spaces/S000200/properties/P000014.md b/spaces/S000200/properties/P000014.md deleted file mode 100644 index b48008995..000000000 --- a/spaces/S000200/properties/P000014.md +++ /dev/null @@ -1,10 +0,0 @@ ---- -space: S000200 -property: P000014 -value: true ---- - -The collection of closed sets is a chain under inclusion; -that is, -for each pair of closed sets, one is contained in the other. -Therefore every subspace is vacuously {P13}. diff --git a/spaces/S000200/properties/P000016.md b/spaces/S000200/properties/P000016.md new file mode 100644 index 000000000..fc6e95572 --- /dev/null +++ b/spaces/S000200/properties/P000016.md @@ -0,0 +1,7 @@ +--- +space: S000200 +property: P000016 +value: true +--- + +Any open cover must contain $\omega$. diff --git a/spaces/S000200/properties/P000039.md b/spaces/S000200/properties/P000039.md deleted file mode 100644 index ee8b420d9..000000000 --- a/spaces/S000200/properties/P000039.md +++ /dev/null @@ -1,9 +0,0 @@ ---- -space: S000200 -property: P000039 -value: true ---- - -The topology is a chain under inclusion; -that is, -for each pair of open sets, one is contained in the other. diff --git a/spaces/S000200/properties/P000086.md b/spaces/S000200/properties/P000086.md deleted file mode 100644 index d470218f4..000000000 --- a/spaces/S000200/properties/P000086.md +++ /dev/null @@ -1,8 +0,0 @@ ---- -space: S000200 -property: P000086 -value: false ---- - -$0$ belongs to only one open set $[0,\infty)$, but $1$ belongs to two open sets $[0,\rightarrow)$ -and $[1,\rightarrow)$. diff --git a/spaces/S000187/properties/P000040.md b/spaces/S000200/properties/P000181.md similarity index 52% rename from spaces/S000187/properties/P000040.md rename to spaces/S000200/properties/P000181.md index 86b6aca72..2018d047e 100644 --- a/spaces/S000187/properties/P000040.md +++ b/spaces/S000200/properties/P000181.md @@ -1,6 +1,6 @@ --- -space: S000187 -property: P000040 +space: S000200 +property: P000181 value: true --- diff --git a/spaces/S000200/properties/P000196.md b/spaces/S000200/properties/P000196.md new file mode 100644 index 000000000..d3e2d8cf9 --- /dev/null +++ b/spaces/S000200/properties/P000196.md @@ -0,0 +1,7 @@ +--- +space: S000200 +property: P000196 +value: true +--- + +By construction. diff --git a/theorems/T000546.md b/theorems/T000546.md new file mode 100644 index 000000000..7a38baf91 --- /dev/null +++ b/theorems/T000546.md @@ -0,0 +1,9 @@ +--- +uid: T000546 +if: + P000196: true +then: + P000039: true +--- + +. diff --git a/theorems/T000547.md b/theorems/T000547.md new file mode 100644 index 000000000..41d9a8861 --- /dev/null +++ b/theorems/T000547.md @@ -0,0 +1,9 @@ +--- +uid: T000547 +if: + P000196: true +then: + P000014: true +--- + +. diff --git a/theorems/T000548.md b/theorems/T000548.md new file mode 100644 index 000000000..aeb145557 --- /dev/null +++ b/theorems/T000548.md @@ -0,0 +1,11 @@ +--- +uid: T000548 +if: + and: + - P000039: true + - P000014: true +then: + P000196: true +--- + +. diff --git a/theorems/T000549.md b/theorems/T000549.md new file mode 100644 index 000000000..31945c166 --- /dev/null +++ b/theorems/T000549.md @@ -0,0 +1,9 @@ +--- +uid: T000549 +if: + P000196: true +then: + P000174: true +--- + +. diff --git a/theorems/T000550.md b/theorems/T000550.md new file mode 100644 index 000000000..0af52f28c --- /dev/null +++ b/theorems/T000550.md @@ -0,0 +1,11 @@ +--- +uid: T000550 +if: + and: + - P000196: true + - P000057: true +then: + P000027: true +--- + +. diff --git a/theorems/T000551.md b/theorems/T000551.md new file mode 100644 index 000000000..bc98aeb31 --- /dev/null +++ b/theorems/T000551.md @@ -0,0 +1,12 @@ +--- +uid: T000551 +if: + and: + - P000196: true + - P000093: true + - P000057: false +then: + P000114: true +--- + +. diff --git a/theorems/T000552.md b/theorems/T000552.md new file mode 100644 index 000000000..2b06d904d --- /dev/null +++ b/theorems/T000552.md @@ -0,0 +1,12 @@ +--- +uid: T000552 +if: + and: + - P000001: true + - P000090: true + - P000027: true +then: + P000057: true +--- + +. From 2d5d204e29377ef2ef2bf7f1d8ae43f8f843d089 Mon Sep 17 00:00:00 2001 From: danflapjax <12000932+danflapjax@users.noreply.github.com> Date: Sun, 13 Oct 2024 21:20:10 -0700 Subject: [PATCH 02/13] add explanations of theorems --- spaces/S000199/properties/P000051.md | 7 +++++++ spaces/S000199/properties/P000136.md | 7 +++++++ spaces/S000199/properties/P000139.md | 7 ------- theorems/T000546.md | 2 +- theorems/T000547.md | 2 +- theorems/T000548.md | 5 ++++- theorems/T000549.md | 2 +- theorems/T000550.md | 2 +- theorems/T000551.md | 2 +- theorems/T000552.md | 12 +++++++----- theorems/T000553.md | 14 ++++++++++++++ 11 files changed, 44 insertions(+), 18 deletions(-) create mode 100644 spaces/S000199/properties/P000051.md create mode 100644 spaces/S000199/properties/P000136.md delete mode 100644 spaces/S000199/properties/P000139.md create mode 100644 theorems/T000553.md diff --git a/spaces/S000199/properties/P000051.md b/spaces/S000199/properties/P000051.md new file mode 100644 index 000000000..ef0361c92 --- /dev/null +++ b/spaces/S000199/properties/P000051.md @@ -0,0 +1,7 @@ +--- +space: S000199 +property: P000051 +value: true +--- +Since $\omega$ is well-ordered, a nonempty set $Y\subseteq\omega$ has a least element $\alpha$. +Then $\alpha$ is isolated in $Y$ since $[0,\alpha+1)\cap Y=\{\alpha\}$. diff --git a/spaces/S000199/properties/P000136.md b/spaces/S000199/properties/P000136.md new file mode 100644 index 000000000..cd74fca5d --- /dev/null +++ b/spaces/S000199/properties/P000136.md @@ -0,0 +1,7 @@ +--- +space: S000199 +property: P000136 +value: true +--- + +Every infinite subspace is homeomorphic to the space itself, and any open cover not containing $\omega$ must be an infinite set of left rays and so cannot have a finite subcover. diff --git a/spaces/S000199/properties/P000139.md b/spaces/S000199/properties/P000139.md deleted file mode 100644 index aede17d35..000000000 --- a/spaces/S000199/properties/P000139.md +++ /dev/null @@ -1,7 +0,0 @@ ---- -space: S000199 -property: P000139 -value: true ---- - -$\{0\}$ is open. diff --git a/theorems/T000546.md b/theorems/T000546.md index 7a38baf91..c806a6ee6 100644 --- a/theorems/T000546.md +++ b/theorems/T000546.md @@ -6,4 +6,4 @@ then: P000039: true --- -. +The open sets are totally ordered by set inclusion and thus no two nonempty ones are disjoint. diff --git a/theorems/T000547.md b/theorems/T000547.md index 41d9a8861..75dec4a9d 100644 --- a/theorems/T000547.md +++ b/theorems/T000547.md @@ -6,4 +6,4 @@ then: P000014: true --- -. +Any {P196} space is trivially {P13} (as there are no disoint closed sets), and the property is hereditary, so all subspaces are as well. diff --git a/theorems/T000548.md b/theorems/T000548.md index aeb145557..ecdd9e1fa 100644 --- a/theorems/T000548.md +++ b/theorems/T000548.md @@ -6,6 +6,9 @@ if: - P000014: true then: P000196: true +refs: +- zb: "0396.54009" + name: On ultrapseudocompact and related spaces (T. Nieminen) --- -. +See theorem 23 at https://www.acadsci.fi/mathematica/Vol03/vol03pp185-205.pdf (reading $T_5$ as {P14}). diff --git a/theorems/T000549.md b/theorems/T000549.md index 31945c166..eccf8b6c1 100644 --- a/theorems/T000549.md +++ b/theorems/T000549.md @@ -6,4 +6,4 @@ then: P000174: true --- -. +The topology is totally ordered by set inclusion, so the set of open neighborhoods of any point is as well. diff --git a/theorems/T000550.md b/theorems/T000550.md index 0af52f28c..25e614d9e 100644 --- a/theorems/T000550.md +++ b/theorems/T000550.md @@ -8,4 +8,4 @@ then: P000027: true --- -. +There can be no more open sets in a {P196} space than there are points. diff --git a/theorems/T000551.md b/theorems/T000551.md index bc98aeb31..7514515a6 100644 --- a/theorems/T000551.md +++ b/theorems/T000551.md @@ -9,4 +9,4 @@ then: P000114: true --- -. +For a totally ordered collection $\mathcal U_i$ of countable sets, $\bigcup_{i\in\mathcal I}\mathcal U_i$ has cardinality at most $\aleph_1$ (as it is the cardinality of the set of all countable ordinal numbers). diff --git a/theorems/T000552.md b/theorems/T000552.md index 2b06d904d..2834aee9a 100644 --- a/theorems/T000552.md +++ b/theorems/T000552.md @@ -2,11 +2,13 @@ uid: T000552 if: and: - - P000001: true - - P000090: true - - P000027: true + - P000196: true + - P000016: true + - P000086: true then: - P000057: true + P000129: true --- -. +If a {P196} space is {P16}, then it must have a second largest open set +(otherwise, $\mathcal T_X\setminus\{X\}$ would be totally ordered with no upper bound and therefore an open cover with no finite subcover). +To be {P86}, no points can lie in this second-largest set, so the space is {P129}. diff --git a/theorems/T000553.md b/theorems/T000553.md new file mode 100644 index 000000000..7d6bf90ad --- /dev/null +++ b/theorems/T000553.md @@ -0,0 +1,14 @@ +--- +uid: T000553 +if: + and: + - P000001: true + - P000090: true + - P000027: true +then: + P000057: true +--- + +In an {P90} space, the smallest basis is the set of smallest neighborhoods of points. +When it is also {P1}, these are all distinct, so they are in bijection with the set of points. +Thus, such a space has a countable basis iff it is countable. From 1e11a925b88b1e5689366ca99f338738a55b43d6 Mon Sep 17 00:00:00 2001 From: danflapjax <12000932+danflapjax@users.noreply.github.com> Date: Sun, 13 Oct 2024 21:53:17 -0700 Subject: [PATCH 03/13] define P196; add spectral theorem --- properties/P000185.md | 2 ++ properties/P000196.md | 8 +++++++- theorems/T000554.md | 15 +++++++++++++++ 3 files changed, 24 insertions(+), 1 deletion(-) create mode 100644 theorems/T000554.md diff --git a/properties/P000185.md b/properties/P000185.md index 2315f680a..540e00090 100644 --- a/properties/P000185.md +++ b/properties/P000185.md @@ -14,5 +14,7 @@ Any of the following equivalent properties holds: - The space's Kolmogorov quotient is {P52}. - The space is the disjoint union of a collection of {P129} spaces. +For further characterizations, see theorem 25 of https://www.acadsci.fi/mathematica/Vol03/vol03pp185-205.pdf. + Defined as example #5 ("Partition Topology") in {{doi:10.1007/978-1-4612-6290-9}}. diff --git a/properties/P000196.md b/properties/P000196.md index 01f89ee37..16ef0f188 100644 --- a/properties/P000196.md +++ b/properties/P000196.md @@ -8,4 +8,10 @@ refs: name: On ultrapseudocompact and related spaces (T. Nieminen) --- -. +Any of the following equivalent properties holds: + +- Any subspace is connected. +- The open sets are totally ordered by set inclusion. +- The specialization preorder is total. + +For further characterizations, see theorem 22 of https://www.acadsci.fi/mathematica/Vol03/vol03pp185-205.pdf. diff --git a/theorems/T000554.md b/theorems/T000554.md new file mode 100644 index 000000000..66b97e672 --- /dev/null +++ b/theorems/T000554.md @@ -0,0 +1,15 @@ +--- +uid: T000528 +if: + and: + - P000196: true + - P000016: true + - P000073: true + - P000090: true +then: + P000075: true +refs: +- doi: 10.1017/9781316543870 + name: Spectral spaces (Dickmann, Schwartz, Tressl) +--- +Shown in Proposition 1.6.7 of {{doi:10.1017/9781316543870}}. From 2fd9998290a687c1a5d506766ed32c66dbd7587f Mon Sep 17 00:00:00 2001 From: danflapjax <12000932+danflapjax@users.noreply.github.com> Date: Sun, 13 Oct 2024 21:58:51 -0700 Subject: [PATCH 04/13] fix uid --- theorems/T000554.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theorems/T000554.md b/theorems/T000554.md index 66b97e672..e2f808bc1 100644 --- a/theorems/T000554.md +++ b/theorems/T000554.md @@ -1,5 +1,5 @@ --- -uid: T000528 +uid: T000554 if: and: - P000196: true From 471c4a153b2b6d6a7457f5f049cf550f3104c368 Mon Sep 17 00:00:00 2001 From: danflapjax <12000932+danflapjax@users.noreply.github.com> Date: Mon, 14 Oct 2024 10:40:49 -0700 Subject: [PATCH 05/13] multiple more theorems --- theorems/T000552.md | 1 - theorems/T000553.md | 11 +++-------- theorems/T000554.md | 2 +- theorems/T000555.md | 11 +++++++++++ theorems/T000556.md | 12 ++++++++++++ theorems/T000557.md | 14 ++++++++++++++ 6 files changed, 41 insertions(+), 10 deletions(-) create mode 100644 theorems/T000555.md create mode 100644 theorems/T000556.md create mode 100644 theorems/T000557.md diff --git a/theorems/T000552.md b/theorems/T000552.md index 2834aee9a..4c3be64db 100644 --- a/theorems/T000552.md +++ b/theorems/T000552.md @@ -8,7 +8,6 @@ if: then: P000129: true --- - If a {P196} space is {P16}, then it must have a second largest open set (otherwise, $\mathcal T_X\setminus\{X\}$ would be totally ordered with no upper bound and therefore an open cover with no finite subcover). To be {P86}, no points can lie in this second-largest set, so the space is {P129}. diff --git a/theorems/T000553.md b/theorems/T000553.md index 7d6bf90ad..6d31adfc9 100644 --- a/theorems/T000553.md +++ b/theorems/T000553.md @@ -1,14 +1,9 @@ --- uid: T000553 if: - and: - - P000001: true - - P000090: true - - P000027: true + P000196: true then: - P000057: true + P000042: true --- -In an {P90} space, the smallest basis is the set of smallest neighborhoods of points. -When it is also {P1}, these are all distinct, so they are in bijection with the set of points. -Thus, such a space has a countable basis iff it is countable. +Every subset of a {P196} space is {P40}, and {T38}. diff --git a/theorems/T000554.md b/theorems/T000554.md index e2f808bc1..487604d1c 100644 --- a/theorems/T000554.md +++ b/theorems/T000554.md @@ -12,4 +12,4 @@ refs: - doi: 10.1017/9781316543870 name: Spectral spaces (Dickmann, Schwartz, Tressl) --- -Shown in Proposition 1.6.7 of {{doi:10.1017/9781316543870}}. +Shown in Proposition 1.6.7 of {{doi:10.1017/9781316543870}}. In particular, it follows that the specialization order is order-isomorphic to a non-limit ordinal. diff --git a/theorems/T000555.md b/theorems/T000555.md new file mode 100644 index 000000000..4f896a3e8 --- /dev/null +++ b/theorems/T000555.md @@ -0,0 +1,11 @@ +--- +uid: T000555 +if: + and: + - P000196: true + - P000176: true +then: + P000044: false +--- + +Since any subset is connected, any partition into non-singletons suffices. diff --git a/theorems/T000556.md b/theorems/T000556.md new file mode 100644 index 000000000..6d869685f --- /dev/null +++ b/theorems/T000556.md @@ -0,0 +1,12 @@ +--- +uid: T000556 +if: + and: + - P000196: true + - P000016: true +then: + P000146: true +--- +If a {P196} space is {P16}, then it must have a second largest open set +(otherwise, $\mathcal T_X\setminus\{X\}$ would be totally ordered with no upper bound and therefore an open cover with no finite subcover). +Thus, any open cover must contain $X$, so it admits a refinement containing $X$ as the only nonempty set. diff --git a/theorems/T000557.md b/theorems/T000557.md new file mode 100644 index 000000000..bd802b06c --- /dev/null +++ b/theorems/T000557.md @@ -0,0 +1,14 @@ +--- +uid: T000557 +if: + and: + - P000001: true + - P000090: true + - P000027: true +then: + P000057: true +--- + +In an {P90} space, the smallest basis is the set of smallest neighborhoods of points. +When it is also {P1}, these are all distinct, so they are in bijection with the set of points. +Thus, such a space has a countable basis iff it is countable. From 6f1a67cff42b411bb55a26bca9aedc809a83ad9a Mon Sep 17 00:00:00 2001 From: danflapjax <12000932+danflapjax@users.noreply.github.com> Date: Wed, 16 Oct 2024 00:47:16 -0700 Subject: [PATCH 06/13] implement suggestions and add new theorems --- properties/P000185.md | 8 +++++--- properties/P000196.md | 7 ++++--- theorems/T000547.md | 2 +- theorems/T000548.md | 4 ++-- theorems/T000549.md | 2 +- theorems/T000550.md | 8 ++++---- theorems/T000555.md | 3 +-- theorems/T000556.md | 10 ++++------ theorems/T000558.md | 10 ++++++++++ theorems/T000559.md | 8 ++++++++ 10 files changed, 40 insertions(+), 22 deletions(-) create mode 100644 theorems/T000558.md create mode 100644 theorems/T000559.md diff --git a/properties/P000185.md b/properties/P000185.md index 540e00090..325c99d54 100644 --- a/properties/P000185.md +++ b/properties/P000185.md @@ -2,8 +2,10 @@ uid: P000185 name: Partition topology refs: - - doi: 10.1007/978-1-4612-6290-9 - name: Counterexamples in Topology +- doi: 10.1007/978-1-4612-6290-9 + name: Counterexamples in Topology +- doi: 10.5186/aasfm.1977.0321 + name: On ultrapseudocompact and related spaces (T. Nieminen) --- Any of the following equivalent properties holds: @@ -14,7 +16,7 @@ Any of the following equivalent properties holds: - The space's Kolmogorov quotient is {P52}. - The space is the disjoint union of a collection of {P129} spaces. -For further characterizations, see theorem 25 of https://www.acadsci.fi/mathematica/Vol03/vol03pp185-205.pdf. +For proof of the equivalences and further characterizations, see section 13 of {{doi:10.5186/aasfm.1977.0321}}. Defined as example #5 ("Partition Topology") in {{doi:10.1007/978-1-4612-6290-9}}. diff --git a/properties/P000196.md b/properties/P000196.md index 16ef0f188..957361c34 100644 --- a/properties/P000196.md +++ b/properties/P000196.md @@ -4,14 +4,15 @@ name: Hereditarily connected aliases: - Totally ordered topology refs: -- zb: "0396.54009" +- doi: 10.5186/aasfm.1977.0321 name: On ultrapseudocompact and related spaces (T. Nieminen) --- Any of the following equivalent properties holds: - Any subspace is connected. -- The open sets are totally ordered by set inclusion. +- The open sets are totally ordered by inclusion. +- The closed sets are totally ordered by inclusion. - The specialization preorder is total. -For further characterizations, see theorem 22 of https://www.acadsci.fi/mathematica/Vol03/vol03pp185-205.pdf. +For proof of the equivalences and further characterizations, see section 12 of {{doi:10.5186/aasfm.1977.0321}}. diff --git a/theorems/T000547.md b/theorems/T000547.md index 75dec4a9d..3803e584f 100644 --- a/theorems/T000547.md +++ b/theorems/T000547.md @@ -6,4 +6,4 @@ then: P000014: true --- -Any {P196} space is trivially {P13} (as there are no disoint closed sets), and the property is hereditary, so all subspaces are as well. +Any {P196} space is trivially {P13} (as there are no disjoint closed sets), so all subspaces are as well. diff --git a/theorems/T000548.md b/theorems/T000548.md index ecdd9e1fa..eb5743d0b 100644 --- a/theorems/T000548.md +++ b/theorems/T000548.md @@ -7,8 +7,8 @@ if: then: P000196: true refs: -- zb: "0396.54009" +- doi: 10.5186/aasfm.1977.0321 name: On ultrapseudocompact and related spaces (T. Nieminen) --- -See theorem 23 at https://www.acadsci.fi/mathematica/Vol03/vol03pp185-205.pdf (reading $T_5$ as {P14}). +See condition (10) of theorem 23 at {{doi:10.5186/aasfm.1977.0321}} (reading $T_5$ as {P14}). diff --git a/theorems/T000549.md b/theorems/T000549.md index eccf8b6c1..69586ecab 100644 --- a/theorems/T000549.md +++ b/theorems/T000549.md @@ -6,4 +6,4 @@ then: P000174: true --- -The topology is totally ordered by set inclusion, so the set of open neighborhoods of any point is as well. +The topology is totally ordered by inclusion, so the set of open neighborhoods of any point is as well. diff --git a/theorems/T000550.md b/theorems/T000550.md index 25e614d9e..5ae939464 100644 --- a/theorems/T000550.md +++ b/theorems/T000550.md @@ -2,10 +2,10 @@ uid: T000550 if: and: - - P000196: true - - P000057: true + - P000193: true + - P000039: true then: - P000027: true + P000146: true --- -There can be no more open sets in a {P196} space than there are points. +In a {P39} space $X$, every nonempty open set is dense, so to admit a shrinking, every open cover must contain $X$. Thus, any open cover admits a clopen refinement. diff --git a/theorems/T000555.md b/theorems/T000555.md index 4f896a3e8..845d480a0 100644 --- a/theorems/T000555.md +++ b/theorems/T000555.md @@ -7,5 +7,4 @@ if: then: P000044: false --- - -Since any subset is connected, any partition into non-singletons suffices. +$X$ has two disjoint subsets, each with at least two points, and each of the subsets is connected. diff --git a/theorems/T000556.md b/theorems/T000556.md index 6d869685f..905ffc09a 100644 --- a/theorems/T000556.md +++ b/theorems/T000556.md @@ -2,11 +2,9 @@ uid: T000556 if: and: - - P000196: true - - P000016: true + - P000146: true + - P000036: true then: - P000146: true + P000016: true --- -If a {P196} space is {P16}, then it must have a second largest open set -(otherwise, $\mathcal T_X\setminus\{X\}$ would be totally ordered with no upper bound and therefore an open cover with no finite subcover). -Thus, any open cover must contain $X$, so it admits a refinement containing $X$ as the only nonempty set. +Any clopen partition of a {P36} space $X$ must contain $X$, so to admit clopen refinements every open cover must contain $X$. Thus, $\{X\}$ is a finite subcover. diff --git a/theorems/T000558.md b/theorems/T000558.md new file mode 100644 index 000000000..0cdd2f179 --- /dev/null +++ b/theorems/T000558.md @@ -0,0 +1,10 @@ +--- +uid: T000558 +if: + and: + - P000146: true + - P000036: true +then: + P000020: true +--- +Any clopen partition of a {P36} space $X$ must contain $X$, so to admit clopen refinements every open cover must contain $X$. Thus, the union of all open sets except for $X$ cannot equal $X$ (as that would be an open cover not containing $X$), so any sequence converges to all points outside of that union (whose only neighborhood is $X$). diff --git a/theorems/T000559.md b/theorems/T000559.md new file mode 100644 index 000000000..1027c0504 --- /dev/null +++ b/theorems/T000559.md @@ -0,0 +1,8 @@ +--- +uid: T000558 +if: + P000040: true +then: + P000088: true +--- +In an {P40} space, since any two nonempty closed sets intersect, any discrete family of closed sets can only contain one nonempty set (which is contained in the open set $X$). From 6f973f05922b7cc5e69333dd83b3ad9aeb941534 Mon Sep 17 00:00:00 2001 From: danflapjax <12000932+danflapjax@users.noreply.github.com> Date: Wed, 16 Oct 2024 00:49:16 -0700 Subject: [PATCH 07/13] fix uid --- theorems/T000559.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theorems/T000559.md b/theorems/T000559.md index 1027c0504..0ce5e776a 100644 --- a/theorems/T000559.md +++ b/theorems/T000559.md @@ -1,5 +1,5 @@ --- -uid: T000558 +uid: T000559 if: P000040: true then: From e50b255fdfb9d8b58112f42d8beb207d3e99e8c9 Mon Sep 17 00:00:00 2001 From: danflapjax <12000932+danflapjax@users.noreply.github.com> Date: Wed, 16 Oct 2024 01:07:19 -0700 Subject: [PATCH 08/13] delete redundant theorem and renumber --- theorems/T000556.md | 4 ++-- theorems/T000558.md | 8 +++----- theorems/T000559.md | 8 -------- 3 files changed, 5 insertions(+), 15 deletions(-) delete mode 100644 theorems/T000559.md diff --git a/theorems/T000556.md b/theorems/T000556.md index 905ffc09a..79a0abbd0 100644 --- a/theorems/T000556.md +++ b/theorems/T000556.md @@ -5,6 +5,6 @@ if: - P000146: true - P000036: true then: - P000016: true + P000020: true --- -Any clopen partition of a {P36} space $X$ must contain $X$, so to admit clopen refinements every open cover must contain $X$. Thus, $\{X\}$ is a finite subcover. +Any clopen partition of a {P36} space $X$ must contain $X$, so to admit clopen refinements every open cover must contain $X$. Thus, the union of all open sets except for $X$ cannot equal $X$ (as that would be an open cover not containing $X$), so any sequence converges to all points outside of that union (whose only neighborhood is $X$). diff --git a/theorems/T000558.md b/theorems/T000558.md index 0cdd2f179..1027c0504 100644 --- a/theorems/T000558.md +++ b/theorems/T000558.md @@ -1,10 +1,8 @@ --- uid: T000558 if: - and: - - P000146: true - - P000036: true + P000040: true then: - P000020: true + P000088: true --- -Any clopen partition of a {P36} space $X$ must contain $X$, so to admit clopen refinements every open cover must contain $X$. Thus, the union of all open sets except for $X$ cannot equal $X$ (as that would be an open cover not containing $X$), so any sequence converges to all points outside of that union (whose only neighborhood is $X$). +In an {P40} space, since any two nonempty closed sets intersect, any discrete family of closed sets can only contain one nonempty set (which is contained in the open set $X$). diff --git a/theorems/T000559.md b/theorems/T000559.md deleted file mode 100644 index 0ce5e776a..000000000 --- a/theorems/T000559.md +++ /dev/null @@ -1,8 +0,0 @@ ---- -uid: T000559 -if: - P000040: true -then: - P000088: true ---- -In an {P40} space, since any two nonempty closed sets intersect, any discrete family of closed sets can only contain one nonempty set (which is contained in the open set $X$). From b32934749bc12c5b35d2898625cb246f07d5b685 Mon Sep 17 00:00:00 2001 From: danflapjax <12000932+danflapjax@users.noreply.github.com> Date: Wed, 16 Oct 2024 13:39:07 -0700 Subject: [PATCH 09/13] Update T000550.md --- theorems/T000550.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/theorems/T000550.md b/theorems/T000550.md index 5ae939464..3ab1ae577 100644 --- a/theorems/T000550.md +++ b/theorems/T000550.md @@ -8,4 +8,5 @@ then: P000146: true --- -In a {P39} space $X$, every nonempty open set is dense, so to admit a shrinking, every open cover must contain $X$. Thus, any open cover admits a clopen refinement. +In a {P39} space $X$, the closure of every nonempty open set is $X$, so any open cover that admits a shrinking must contain $X$ (as otherwise each of its open sets could only contain the closure of $\varnothing$). +Thus, any such open cover admits an open refinement to the partition $\{X\}$. From de62c54dee91acbc2a5b082ea6f6edad4ec16322 Mon Sep 17 00:00:00 2001 From: danflapjax <12000932+danflapjax@users.noreply.github.com> Date: Wed, 16 Oct 2024 19:18:28 -0700 Subject: [PATCH 10/13] Strengthen T552 --- theorems/T000552.md | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/theorems/T000552.md b/theorems/T000552.md index 4c3be64db..ab728be17 100644 --- a/theorems/T000552.md +++ b/theorems/T000552.md @@ -2,12 +2,10 @@ uid: T000552 if: and: - - P000196: true - - P000016: true + - P000146: true + - P000036: true - P000086: true then: P000129: true --- -If a {P196} space is {P16}, then it must have a second largest open set -(otherwise, $\mathcal T_X\setminus\{X\}$ would be totally ordered with no upper bound and therefore an open cover with no finite subcover). -To be {P86}, no points can lie in this second-largest set, so the space is {P129}. +Any clopen partition of a {P36} space $X$ must contain $X$, so to admit clopen refinements every open cover must contain $X$. Thus, the union of all open sets except for $X$ cannot equal $X$ (as that would be an open cover not containing $X$), so some points have $X$ as their only neighborhood. By homogeneity, this must then be true of all points, i.e. the space is {P129}. From aee37d48e70e8f4a98e1a6593cf4a879b041df55 Mon Sep 17 00:00:00 2001 From: Patrick Rabau <70125716+prabau@users.noreply.github.com> Date: Thu, 17 Oct 2024 00:39:23 -0400 Subject: [PATCH 11/13] T552 fix --- theorems/T000552.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theorems/T000552.md b/theorems/T000552.md index ab728be17..532f52226 100644 --- a/theorems/T000552.md +++ b/theorems/T000552.md @@ -8,4 +8,4 @@ if: then: P000129: true --- -Any clopen partition of a {P36} space $X$ must contain $X$, so to admit clopen refinements every open cover must contain $X$. Thus, the union of all open sets except for $X$ cannot equal $X$ (as that would be an open cover not containing $X$), so some points have $X$ as their only neighborhood. By homogeneity, this must then be true of all points, i.e. the space is {P129}. +Any clopen partition of a {P36} space $X$ must contain $X$, so every open cover admitting a clopen partition as refinement must contain $X$. Thus, the union of all open sets except for $X$ cannot equal $X$ (as that would be an open cover not containing $X$), so some points have $X$ as their only neighborhood. By homogeneity, this must then be true of all points, i.e. the space is {P129}. From a4274f868044d3617fd832478753a58f281e6b8f Mon Sep 17 00:00:00 2001 From: Patrick Rabau <70125716+prabau@users.noreply.github.com> Date: Thu, 17 Oct 2024 15:35:32 -0400 Subject: [PATCH 12/13] remove T558 --- theorems/T000558.md | 8 -------- 1 file changed, 8 deletions(-) delete mode 100644 theorems/T000558.md diff --git a/theorems/T000558.md b/theorems/T000558.md deleted file mode 100644 index 1027c0504..000000000 --- a/theorems/T000558.md +++ /dev/null @@ -1,8 +0,0 @@ ---- -uid: T000558 -if: - P000040: true -then: - P000088: true ---- -In an {P40} space, since any two nonempty closed sets intersect, any discrete family of closed sets can only contain one nonempty set (which is contained in the open set $X$). From 648cb44dd76234a49f23672aa53a49bc20fae39c Mon Sep 17 00:00:00 2001 From: Patrick Rabau <70125716+prabau@users.noreply.github.com> Date: Thu, 17 Oct 2024 16:18:54 -0400 Subject: [PATCH 13/13] T551 and T554 changes --- theorems/T000551.md | 2 +- theorems/T000554.md | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/theorems/T000551.md b/theorems/T000551.md index 7514515a6..1c5774c8a 100644 --- a/theorems/T000551.md +++ b/theorems/T000551.md @@ -9,4 +9,4 @@ then: P000114: true --- -For a totally ordered collection $\mathcal U_i$ of countable sets, $\bigcup_{i\in\mathcal I}\mathcal U_i$ has cardinality at most $\aleph_1$ (as it is the cardinality of the set of all countable ordinal numbers). +By {P93} choose a countable open neighborhood of each point. So $X$ can be covered by a family of countable sets, forming a chain under inclusion by {P196}. And the union of a chain of countable sets has cardinality at most $\aleph_1$ (see {{mathse:342091}} for example). diff --git a/theorems/T000554.md b/theorems/T000554.md index 487604d1c..fc39050ba 100644 --- a/theorems/T000554.md +++ b/theorems/T000554.md @@ -12,4 +12,6 @@ refs: - doi: 10.1017/9781316543870 name: Spectral spaces (Dickmann, Schwartz, Tressl) --- -Shown in Proposition 1.6.7 of {{doi:10.1017/9781316543870}}. In particular, it follows that the specialization order is order-isomorphic to a non-limit ordinal. +Shown in Proposition 1.6.7 of {{doi:10.1017/9781316543870}}. + +Furthermore, if the space is nonempty, its specialization order is order-isomorphic to a successor ordinal $\lambda$ and the space is homeomorphic to $\lambda$ with the left-ray topology having the collection of intervals $[0,\alpha]$ ($\alpha\in\lambda$) as a base.