From 5b54b96d6479fda92fec16d0290e7497063001c3 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Fri, 29 Aug 2025 08:17:30 +0200 Subject: [PATCH 01/19] Mysior plane initialization --- spaces/S000211/README.md | 11 +++++++++++ spaces/S000211/properties/P000006.md | 10 ++++++++++ spaces/S000211/properties/P000065.md | 7 +++++++ spaces/S000211/properties/P000162.md | 10 ++++++++++ 4 files changed, 38 insertions(+) create mode 100644 spaces/S000211/README.md create mode 100644 spaces/S000211/properties/P000006.md create mode 100644 spaces/S000211/properties/P000065.md create mode 100644 spaces/S000211/properties/P000162.md diff --git a/spaces/S000211/README.md b/spaces/S000211/README.md new file mode 100644 index 0000000000..6036db699e --- /dev/null +++ b/spaces/S000211/README.md @@ -0,0 +1,11 @@ +--- +uid: S000211 +name: Mysior plane +refs: + - zb: "1265.54111" + name: r-realcompact spaces (Bhattacharya, Lipika) +--- + +For $X = \mathbb{R}^2$ let $(x, y)\in X$ for $y\neq 0$ be isolated, and if $y = 0$ let $$U_n(x) = \{(x, y): |y| < 1/n\}\cup \{(x+y+1, y): 0 < y < 1/n\}\cup \{(x+y+\sqrt{2}, -y) : 0 < y < 1/n\}$$ be open neighbourhoods of $(x, 0)$. + +Defined as example 5 of {{zb:1265.54111}}. diff --git a/spaces/S000211/properties/P000006.md b/spaces/S000211/properties/P000006.md new file mode 100644 index 0000000000..96e751fe24 --- /dev/null +++ b/spaces/S000211/properties/P000006.md @@ -0,0 +1,10 @@ +--- +space: S000211 +property: P000006 +value: true +refs: + - mathse: 4718866 + name: Mysior plane is not realcompact +--- + +Proved in {{mathse:4718866}}. diff --git a/spaces/S000211/properties/P000065.md b/spaces/S000211/properties/P000065.md new file mode 100644 index 0000000000..574e396e3b --- /dev/null +++ b/spaces/S000211/properties/P000065.md @@ -0,0 +1,7 @@ +--- +space: S000211 +property: P000065 +value: true +--- + +By definition. diff --git a/spaces/S000211/properties/P000162.md b/spaces/S000211/properties/P000162.md new file mode 100644 index 0000000000..b8f16ecd7a --- /dev/null +++ b/spaces/S000211/properties/P000162.md @@ -0,0 +1,10 @@ +--- +space: S000211 +property: P000162 +value: false +refs: + - mathse: 4718866 + name: Mysior plane is not realcompact +--- + +Proved in {{mathse:4718866}}. From b105c274bdeabe77cd818f916f0c82d6c0966603 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Fri, 29 Aug 2025 20:59:48 +0200 Subject: [PATCH 02/19] update space id --- spaces/{S000211 => S000215}/README.md | 2 +- spaces/{S000211 => S000215}/properties/P000006.md | 2 +- spaces/{S000211 => S000215}/properties/P000065.md | 2 +- spaces/{S000211 => S000215}/properties/P000162.md | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) rename spaces/{S000211 => S000215}/README.md (96%) rename spaces/{S000211 => S000215}/properties/P000006.md (90%) rename spaces/{S000211 => S000215}/properties/P000065.md (78%) rename spaces/{S000211 => S000215}/properties/P000162.md (90%) diff --git a/spaces/S000211/README.md b/spaces/S000215/README.md similarity index 96% rename from spaces/S000211/README.md rename to spaces/S000215/README.md index 6036db699e..0304911504 100644 --- a/spaces/S000211/README.md +++ b/spaces/S000215/README.md @@ -1,5 +1,5 @@ --- -uid: S000211 +uid: S000215 name: Mysior plane refs: - zb: "1265.54111" diff --git a/spaces/S000211/properties/P000006.md b/spaces/S000215/properties/P000006.md similarity index 90% rename from spaces/S000211/properties/P000006.md rename to spaces/S000215/properties/P000006.md index 96e751fe24..1a1ac03f7e 100644 --- a/spaces/S000211/properties/P000006.md +++ b/spaces/S000215/properties/P000006.md @@ -1,5 +1,5 @@ --- -space: S000211 +space: S000215 property: P000006 value: true refs: diff --git a/spaces/S000211/properties/P000065.md b/spaces/S000215/properties/P000065.md similarity index 78% rename from spaces/S000211/properties/P000065.md rename to spaces/S000215/properties/P000065.md index 574e396e3b..b894db47a6 100644 --- a/spaces/S000211/properties/P000065.md +++ b/spaces/S000215/properties/P000065.md @@ -1,5 +1,5 @@ --- -space: S000211 +space: S000215 property: P000065 value: true --- diff --git a/spaces/S000211/properties/P000162.md b/spaces/S000215/properties/P000162.md similarity index 90% rename from spaces/S000211/properties/P000162.md rename to spaces/S000215/properties/P000162.md index b8f16ecd7a..e592b0d950 100644 --- a/spaces/S000211/properties/P000162.md +++ b/spaces/S000215/properties/P000162.md @@ -1,5 +1,5 @@ --- -space: S000211 +space: S000215 property: P000162 value: false refs: From 668ad6a7590d1033b6f5de54bf30c30636f90827 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Sat, 30 Aug 2025 10:45:54 +0200 Subject: [PATCH 03/19] add some properties --- spaces/S000215/properties/P000007.md | 7 +++++++ spaces/S000215/properties/P000022.md | 10 ++++++++++ spaces/S000215/properties/P000051.md | 7 +++++++ spaces/S000215/properties/P000198.md | 7 +++++++ 4 files changed, 31 insertions(+) create mode 100644 spaces/S000215/properties/P000007.md create mode 100644 spaces/S000215/properties/P000022.md create mode 100644 spaces/S000215/properties/P000051.md create mode 100644 spaces/S000215/properties/P000198.md diff --git a/spaces/S000215/properties/P000007.md b/spaces/S000215/properties/P000007.md new file mode 100644 index 0000000000..ca686034ec --- /dev/null +++ b/spaces/S000215/properties/P000007.md @@ -0,0 +1,7 @@ +--- +space: S000215 +property: P000007 +value: false +--- + +Let $A\subseteq \mathbb{R}$ be uncountable and $B = \{a+1 : a\in A\}$. If $A\times \{0\}\subseteq U$ and $B\times \{0\}\subseteq V$ where $U$ and $V$ are open, there exists uncountable $B_0\subseteq B$ and $n$ such that $B_0\times (-1/n, 1/n)\subseteq V$. Let $A_0 = \{b-1 : b\in B_0\}$. There exists uncountable $A_1\subseteq A_0$ and $m$ such that $\{(a+y+1, y) : a\in A_1, 0 < y < 1/m\}\subseteq U$. Let $B_1 = \{a+1 : a\in A_1\}$. Then $B_1\times (-1/n, 1/n)$ and $\{(a+y+1, y) : a\in A_1, 0 < y < 1/m\}$ are easily seen to intersect by taking a limit point $a\in A_1'\cap A_1$. Indeed, if $a_k\in A_1$ and $a_k\to a$ then take $k_1, k_2$ such that $0 < |a_{k_1}-a_{k_2}|< \min(1/n, 1/m)$, say $a_{k_1} < a_{k_2}$, then $\{(a_{k_1}+y+1, y) : 0 < y < 1/m\}$ and $\{a_{k_2}+1\} \times (-1/n, 1/n)$ intersect and so $U\cap V\neq\emptyset$, so the disjoint closed sets $A\times \{0\}$ and $B\times \{0\}$ can't be separated by open sets. diff --git a/spaces/S000215/properties/P000022.md b/spaces/S000215/properties/P000022.md new file mode 100644 index 0000000000..bd4b24a164 --- /dev/null +++ b/spaces/S000215/properties/P000022.md @@ -0,0 +1,10 @@ +--- +space: S000215 +property: P000022 +value: false +refs: + - mathse: 4718866 + name: Mysior plane is not realcompact +--- + +The function $f:X\to\mathbb{R}$ defined by $f(x, y) = \begin{cases} x, & y = 1 \\ 0, & y\neq 1 \end{cases}$ is continuous and unbounded. diff --git a/spaces/S000215/properties/P000051.md b/spaces/S000215/properties/P000051.md new file mode 100644 index 0000000000..eaf6d0a090 --- /dev/null +++ b/spaces/S000215/properties/P000051.md @@ -0,0 +1,7 @@ +--- +space: S000215 +property: P000051 +value: true +--- + +If $Y\subseteq X$ is non-empty then it either $(x, y)\in Y$ for some $y\neq 0$ so that $(x, y)$ is isolated point of $Y$, or $Y\subseteq \mathbb{R}\times \{0\}$ and since $U_n(x)\cap \mathbb{R}\times \{0\} = \{(x, 0)\}$ it follows that $Y$ is discrete. diff --git a/spaces/S000215/properties/P000198.md b/spaces/S000215/properties/P000198.md new file mode 100644 index 0000000000..348cb862d7 --- /dev/null +++ b/spaces/S000215/properties/P000198.md @@ -0,0 +1,7 @@ +--- +space: S000215 +property: P000198 +value: false +--- + +$\mathbb{R}\times [1, \infty)$ is an uncountable closed discrete subset of $X$ From da1f7a4daa75a1fa4a7f361e3dcee5c6535bef89 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Sat, 6 Sep 2025 16:12:31 +0200 Subject: [PATCH 04/19] not weakly Lindelof --- spaces/S000215/properties/P000062.md | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 spaces/S000215/properties/P000062.md diff --git a/spaces/S000215/properties/P000062.md b/spaces/S000215/properties/P000062.md new file mode 100644 index 0000000000..a6e29d534b --- /dev/null +++ b/spaces/S000215/properties/P000062.md @@ -0,0 +1,7 @@ +--- +space: S000215 +property: P000062 +value: false +--- + +The open cover $\mathcal{U} = \{\mathbb{R}\times (-1, 1)\}\cup \{\{x\} : x\in X\setminus (\mathbb{R}\times (-1, 1))\}$ is a partition, and if there is a subfamily $\mathcal{V}\subseteq \mathcal{U}$ such that $\bigcup \mathcal{V}$ is dense, then $\mathcal{V} = \mathcal{U}$. Since $\mathcal{U}$ is uncountable, $X$ is not {P62}. From b41fcf81176a61fbafe561299a9eeff4a7b729eb Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Sat, 6 Sep 2025 16:34:20 +0200 Subject: [PATCH 05/19] locally metrizable --- spaces/S000215/properties/P000082.md | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 spaces/S000215/properties/P000082.md diff --git a/spaces/S000215/properties/P000082.md b/spaces/S000215/properties/P000082.md new file mode 100644 index 0000000000..5d1a1dd821 --- /dev/null +++ b/spaces/S000215/properties/P000082.md @@ -0,0 +1,7 @@ +--- +space: S000215 +property: P000082 +value: true +--- + +If $(x, y)\in X$ and $y\neq 0$, then $(x, y)$ is isolated and so has a metrizable neighbourhood. If $y = 0$ then from {T643} the neighourhood $U_n(x)$ of $(x, y)$ is metrizable. From d034ba52b32a7ffa8371bd81a7f91e3f55517cb8 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Sun, 7 Sep 2025 07:51:38 +0200 Subject: [PATCH 06/19] Cech complete and not locally compact --- spaces/S000215/properties/P000023.md | 7 +++++++ spaces/S000215/properties/P000063.md | 7 +++++++ 2 files changed, 14 insertions(+) create mode 100644 spaces/S000215/properties/P000023.md create mode 100644 spaces/S000215/properties/P000063.md diff --git a/spaces/S000215/properties/P000023.md b/spaces/S000215/properties/P000023.md new file mode 100644 index 0000000000..e7d74624d7 --- /dev/null +++ b/spaces/S000215/properties/P000023.md @@ -0,0 +1,7 @@ +--- +space: S000215 +property: P000023 +value: false +--- + +If $V$ is a compact neighbourhood of $(x, 0)$, then $U_n(x)\subseteq V$ for some $n$. Since $U_n(x)$ is closed, it follows that it must be compact. But since $U_{n+1}(x)\setminus U_n(x)$ is a discrete open set of size $\mathfrak{c}$, the family $\mathcal{U} = \{U_{n+1}(x)\} \cup \{\{y\}: y\in U_n(x)\setminus U_{n+1}(x) \}$ is an open partition of $U_n(x)$ without a finite subcover. diff --git a/spaces/S000215/properties/P000063.md b/spaces/S000215/properties/P000063.md new file mode 100644 index 0000000000..4340de37d8 --- /dev/null +++ b/spaces/S000215/properties/P000063.md @@ -0,0 +1,7 @@ +--- +space: S000215 +property: P000063 +value: true +--- + +Let $\mathcal{U}_n = \{U_n(x) : x\in\mathbb{R}\} \cup \{\{y\} : y\in X\setminus \bigcup_n U_n(x)\}$. Suppose that $\mathcal{F}$ is a family of closed subsets of $X$ with finite intersection property, and such that for each $n$ there exists $F_n\in\mathcal{F}$ with $F_n\subseteq U$ for some $U\in\mathcal{U}_n$. If $U = \{y\}$, then $F_n = \{y\}$ and so $y\in \bigcap \mathcal{F}$. So we can assume that $F_n\subseteq U_n(x_n)$ where $x_n\in\mathbb{R}$. If $(x_n, 0)\notin F_n$, then $U_k(x_n)\cap F_n = \emptyset$ for some $k$, and so $F_n\subseteq X\setminus (\mathbb{R}\times (-\frac{1}{k}, \frac{1}{k}))$. And since $F_k\subseteq U_k(x_k)\subseteq \mathbb{R}\times (-\frac{1}{k}, \frac{1}{k})$, we must have $F_k\cap F_n = \emptyset$, which is a contradiction. So $x_n\in F_n$ for all $n$. Since $F_n\cap F_m\neq\emptyset$ it follows that $U_n(x_n)\cap U_m(x_m)\neq\emptyset$ and so $x_n = x_m$ or $1 < |x_n-x_m|\leq \sqrt{2}$. But as $[-\sqrt{2}+x_1, \sqrt{2}+x_1]$ is totally bounded, the set $\{x_n : n\in\mathbb{N}\}$ must be finite, and so there is $x\in\mathbb{R}$ such that $x_n = x$ for infinitely many $x$. If $F\in\mathcal{F}$, then $U_n(x)\cap F\supseteq F_n\cap F\neq\emptyset$ for infinitely many $n$, and so $U_n(x)\cap F\neq\emptyset$ for all $n$, which implies $(x, 0)\in F$ for all $F\in\mathcal{F}$ or in other words $(x, 0)\in\bigcap\mathcal{F}$. From 594ca51436eb0a0704aeb2beff443ebb491437de Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Sun, 7 Sep 2025 08:36:16 +0200 Subject: [PATCH 07/19] developable --- spaces/S000215/properties/P000110.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 spaces/S000215/properties/P000110.md diff --git a/spaces/S000215/properties/P000110.md b/spaces/S000215/properties/P000110.md new file mode 100644 index 0000000000..b09510bc0c --- /dev/null +++ b/spaces/S000215/properties/P000110.md @@ -0,0 +1,14 @@ +--- +space: S000215 +property: P000110 +value: true +refs: + - doi: 10.2991/978-94-6239-216-8 + name: Generalized Metric Spaces and Mappings (S. Lin, Z. Yun) +--- + +By theorem 1.2.13 of {{doi:10.2991/978-94-6239-216-8}} it suffices to show that $X$ is quasi-developable and a {P132}. + +If $A\subseteq X$, write $A = A_0\cup A_1$ where $A_0\subseteq \mathbb{R}\times \{0\}$ and $A_1\subseteq \mathbb{R}\times (\mathbb{R}\setminus \{0\})$. Then $A_1$ is open and $A_0 = \bigcap_n \bigcup_{x\in A_0} U_n(x)$ so that $A$ is a union of two $G_\delta$-sets, and so $G_\delta$ itself, showing that any subset of $X$ is a $G_\delta$-set. In particular $X$ is a {P132}. + +To show $X$ is quasi-developable, let $\mathcal{V} = \{\{x\} : x\in X\setminus (\mathbb{R}\times \{0\})\}$ and $\mathcal{A}_n^i = \{U_n(x) : x\in [3m+i, 3m+i+1), m\in\mathbb{N}\}$ where $i = 0, 1, 2$. Then $\{\mathcal{V}\}\cup \{\mathcal{A}_n^i : n\in\mathbb{N}, i = 0, 1, 2\}$ is a quasi-development for $X$. From 70a43ef73d47098686709b4b9603d213524f2e51 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Sun, 7 Sep 2025 08:53:00 +0200 Subject: [PATCH 08/19] metacompact --- spaces/S000215/properties/P000031.md | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 spaces/S000215/properties/P000031.md diff --git a/spaces/S000215/properties/P000031.md b/spaces/S000215/properties/P000031.md new file mode 100644 index 0000000000..5de623b69d --- /dev/null +++ b/spaces/S000215/properties/P000031.md @@ -0,0 +1,7 @@ +--- +space: S000215 +property: P000031 +value: true +--- + +If $\mathcal{U}$ is an open cover of $X$, for each $x\in \mathbb{R}$ pick $n(x)$ such that $U_{n(x)}(x)\subseteq U$ for some $U\in\mathcal{U}$. Let $\mathcal{V} = \{U_{n(x)}(x) : x\in \mathbb{R}\}\cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_{n(x)}(x)\}$, then $\mathcal{V}$ is an open refinement of $\mathcal{U}$, and any point of $X$ is contained in at most two elements of $\mathcal{V}$. From d8ffa8974e28236a3d69ebefa187aac4fe0eb4d6 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Sun, 7 Sep 2025 10:33:56 +0200 Subject: [PATCH 09/19] delete normal --- spaces/S000215/properties/P000007.md | 7 ------- 1 file changed, 7 deletions(-) delete mode 100644 spaces/S000215/properties/P000007.md diff --git a/spaces/S000215/properties/P000007.md b/spaces/S000215/properties/P000007.md deleted file mode 100644 index ca686034ec..0000000000 --- a/spaces/S000215/properties/P000007.md +++ /dev/null @@ -1,7 +0,0 @@ ---- -space: S000215 -property: P000007 -value: false ---- - -Let $A\subseteq \mathbb{R}$ be uncountable and $B = \{a+1 : a\in A\}$. If $A\times \{0\}\subseteq U$ and $B\times \{0\}\subseteq V$ where $U$ and $V$ are open, there exists uncountable $B_0\subseteq B$ and $n$ such that $B_0\times (-1/n, 1/n)\subseteq V$. Let $A_0 = \{b-1 : b\in B_0\}$. There exists uncountable $A_1\subseteq A_0$ and $m$ such that $\{(a+y+1, y) : a\in A_1, 0 < y < 1/m\}\subseteq U$. Let $B_1 = \{a+1 : a\in A_1\}$. Then $B_1\times (-1/n, 1/n)$ and $\{(a+y+1, y) : a\in A_1, 0 < y < 1/m\}$ are easily seen to intersect by taking a limit point $a\in A_1'\cap A_1$. Indeed, if $a_k\in A_1$ and $a_k\to a$ then take $k_1, k_2$ such that $0 < |a_{k_1}-a_{k_2}|< \min(1/n, 1/m)$, say $a_{k_1} < a_{k_2}$, then $\{(a_{k_1}+y+1, y) : 0 < y < 1/m\}$ and $\{a_{k_2}+1\} \times (-1/n, 1/n)$ intersect and so $U\cap V\neq\emptyset$, so the disjoint closed sets $A\times \{0\}$ and $B\times \{0\}$ can't be separated by open sets. From 17f4f21df3ba965530c553026f1c4916b2409432 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Mon, 8 Sep 2025 08:33:26 +0200 Subject: [PATCH 10/19] zero dimensional --- spaces/S000215/properties/P000050.md | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 spaces/S000215/properties/P000050.md diff --git a/spaces/S000215/properties/P000050.md b/spaces/S000215/properties/P000050.md new file mode 100644 index 0000000000..e562b9850c --- /dev/null +++ b/spaces/S000215/properties/P000050.md @@ -0,0 +1,7 @@ +--- +space: S000215 +property: P000050 +value: true +--- + +The neighbourhood basis $U_n(x)$ of $(x, 0)$ is clopen for each $x\in \mathbb{R}$. From e4b3c580b97b035af8f26b26275f1364a828fb12 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Mon, 8 Sep 2025 08:57:56 +0200 Subject: [PATCH 11/19] cozero complemented --- spaces/S000215/properties/P000061.md | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 spaces/S000215/properties/P000061.md diff --git a/spaces/S000215/properties/P000061.md b/spaces/S000215/properties/P000061.md new file mode 100644 index 0000000000..bfa1349585 --- /dev/null +++ b/spaces/S000215/properties/P000061.md @@ -0,0 +1,7 @@ +--- +space: S000215 +property: P000061 +value: true +--- + +Note that if $V\subseteq X\setminus (\mathbb{R}\times \{0\})$ then $V = \bigcup_n V_n$ where $V_n = V\cap (X\setminus \mathbb{R}\times (-\frac{1}{n}, \frac{1}{n}))$ and $V_n$ are clopen, so that $U$ is a cozero set. If now $U\subseteq X$, let $V = X\setminus (U\cup \mathbb{R}\times \{0\})$, then $V$ is a cozero set and $V\cup U$ contains $X\setminus (\mathbb{R}\times \{0\})$ which is dense in $X$, so that $U\cup V$ is dense in $X$. From 825be032578ce9bcee4fb3455bfa8be30fd30b61 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Mon, 8 Sep 2025 09:00:49 +0200 Subject: [PATCH 12/19] locally countable --- spaces/S000215/properties/P000093.md | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 spaces/S000215/properties/P000093.md diff --git a/spaces/S000215/properties/P000093.md b/spaces/S000215/properties/P000093.md new file mode 100644 index 0000000000..71673e8fbf --- /dev/null +++ b/spaces/S000215/properties/P000093.md @@ -0,0 +1,7 @@ +--- +space: S000215 +property: P00093 +value: false +--- + +The neighbourhoods $U_n(x)$ of $(x, 0)$ are uncountable. From 96973c39bbcea5f1c053005108b57880f8b12e6e Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Mon, 8 Sep 2025 11:49:49 +0200 Subject: [PATCH 13/19] moved Tychonoff to cozero complemented --- spaces/S000215/properties/P000006.md | 10 ---------- spaces/S000215/properties/P000061.md | 5 +++++ 2 files changed, 5 insertions(+), 10 deletions(-) delete mode 100644 spaces/S000215/properties/P000006.md diff --git a/spaces/S000215/properties/P000006.md b/spaces/S000215/properties/P000006.md deleted file mode 100644 index 1a1ac03f7e..0000000000 --- a/spaces/S000215/properties/P000006.md +++ /dev/null @@ -1,10 +0,0 @@ ---- -space: S000215 -property: P000006 -value: true -refs: - - mathse: 4718866 - name: Mysior plane is not realcompact ---- - -Proved in {{mathse:4718866}}. diff --git a/spaces/S000215/properties/P000061.md b/spaces/S000215/properties/P000061.md index bfa1349585..21ec1b849a 100644 --- a/spaces/S000215/properties/P000061.md +++ b/spaces/S000215/properties/P000061.md @@ -2,6 +2,11 @@ space: S000215 property: P000061 value: true +refs: + - mathse: 4718866 + name: Mysior plane is not realcompact --- +{P6} was proven in {{mathse:4718866}}. + Note that if $V\subseteq X\setminus (\mathbb{R}\times \{0\})$ then $V = \bigcup_n V_n$ where $V_n = V\cap (X\setminus \mathbb{R}\times (-\frac{1}{n}, \frac{1}{n}))$ and $V_n$ are clopen, so that $U$ is a cozero set. If now $U\subseteq X$, let $V = X\setminus (U\cup \mathbb{R}\times \{0\})$, then $V$ is a cozero set and $V\cup U$ contains $X\setminus (\mathbb{R}\times \{0\})$ which is dense in $X$, so that $U\cup V$ is dense in $X$. From b36f02595d574c7be6dce6526bc53250564e8d99 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Mon, 8 Sep 2025 11:52:30 +0200 Subject: [PATCH 14/19] slight change --- spaces/S000215/properties/P000061.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spaces/S000215/properties/P000061.md b/spaces/S000215/properties/P000061.md index 21ec1b849a..79fa7bd056 100644 --- a/spaces/S000215/properties/P000061.md +++ b/spaces/S000215/properties/P000061.md @@ -7,6 +7,6 @@ refs: name: Mysior plane is not realcompact --- -{P6} was proven in {{mathse:4718866}}. +The property {P6} was proven in {{mathse:4718866}}. Note that if $V\subseteq X\setminus (\mathbb{R}\times \{0\})$ then $V = \bigcup_n V_n$ where $V_n = V\cap (X\setminus \mathbb{R}\times (-\frac{1}{n}, \frac{1}{n}))$ and $V_n$ are clopen, so that $U$ is a cozero set. If now $U\subseteq X$, let $V = X\setminus (U\cup \mathbb{R}\times \{0\})$, then $V$ is a cozero set and $V\cup U$ contains $X\setminus (\mathbb{R}\times \{0\})$ which is dense in $X$, so that $U\cup V$ is dense in $X$. From 89efc2667585326d240a02639deccfb055c4c617 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Mon, 8 Sep 2025 11:53:47 +0200 Subject: [PATCH 15/19] added missing 0 --- spaces/S000215/properties/P000093.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spaces/S000215/properties/P000093.md b/spaces/S000215/properties/P000093.md index 71673e8fbf..e4b9dc3f19 100644 --- a/spaces/S000215/properties/P000093.md +++ b/spaces/S000215/properties/P000093.md @@ -1,6 +1,6 @@ --- space: S000215 -property: P00093 +property: P000093 value: false --- From a668e13031225c8620f7e83c4b91daf5caa59480 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Mon, 8 Sep 2025 16:02:43 +0200 Subject: [PATCH 16/19] added para-Lindelof, fixed index --- spaces/S000215/properties/P000063.md | 2 +- spaces/S000215/properties/P000105.md | 7 +++++++ 2 files changed, 8 insertions(+), 1 deletion(-) create mode 100644 spaces/S000215/properties/P000105.md diff --git a/spaces/S000215/properties/P000063.md b/spaces/S000215/properties/P000063.md index 4340de37d8..7c485fbe6c 100644 --- a/spaces/S000215/properties/P000063.md +++ b/spaces/S000215/properties/P000063.md @@ -4,4 +4,4 @@ property: P000063 value: true --- -Let $\mathcal{U}_n = \{U_n(x) : x\in\mathbb{R}\} \cup \{\{y\} : y\in X\setminus \bigcup_n U_n(x)\}$. Suppose that $\mathcal{F}$ is a family of closed subsets of $X$ with finite intersection property, and such that for each $n$ there exists $F_n\in\mathcal{F}$ with $F_n\subseteq U$ for some $U\in\mathcal{U}_n$. If $U = \{y\}$, then $F_n = \{y\}$ and so $y\in \bigcap \mathcal{F}$. So we can assume that $F_n\subseteq U_n(x_n)$ where $x_n\in\mathbb{R}$. If $(x_n, 0)\notin F_n$, then $U_k(x_n)\cap F_n = \emptyset$ for some $k$, and so $F_n\subseteq X\setminus (\mathbb{R}\times (-\frac{1}{k}, \frac{1}{k}))$. And since $F_k\subseteq U_k(x_k)\subseteq \mathbb{R}\times (-\frac{1}{k}, \frac{1}{k})$, we must have $F_k\cap F_n = \emptyset$, which is a contradiction. So $x_n\in F_n$ for all $n$. Since $F_n\cap F_m\neq\emptyset$ it follows that $U_n(x_n)\cap U_m(x_m)\neq\emptyset$ and so $x_n = x_m$ or $1 < |x_n-x_m|\leq \sqrt{2}$. But as $[-\sqrt{2}+x_1, \sqrt{2}+x_1]$ is totally bounded, the set $\{x_n : n\in\mathbb{N}\}$ must be finite, and so there is $x\in\mathbb{R}$ such that $x_n = x$ for infinitely many $x$. If $F\in\mathcal{F}$, then $U_n(x)\cap F\supseteq F_n\cap F\neq\emptyset$ for infinitely many $n$, and so $U_n(x)\cap F\neq\emptyset$ for all $n$, which implies $(x, 0)\in F$ for all $F\in\mathcal{F}$ or in other words $(x, 0)\in\bigcap\mathcal{F}$. +Let $\mathcal{U}_n = \{U_n(x) : x\in\mathbb{R}\} \cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_n(x)\}$. Suppose that $\mathcal{F}$ is a family of closed subsets of $X$ with finite intersection property, and such that for each $n$ there exists $F_n\in\mathcal{F}$ with $F_n\subseteq U$ for some $U\in\mathcal{U}_n$. If $U = \{y\}$, then $F_n = \{y\}$ and so $y\in \bigcap \mathcal{F}$. So we can assume that $F_n\subseteq U_n(x_n)$ where $x_n\in\mathbb{R}$. If $(x_n, 0)\notin F_n$, then $U_k(x_n)\cap F_n = \emptyset$ for some $k$, and so $F_n\subseteq X\setminus (\mathbb{R}\times (-\frac{1}{k}, \frac{1}{k}))$. And since $F_k\subseteq U_k(x_k)\subseteq \mathbb{R}\times (-\frac{1}{k}, \frac{1}{k})$, we must have $F_k\cap F_n = \emptyset$, which is a contradiction. So $x_n\in F_n$ for all $n$. Since $F_n\cap F_m\neq\emptyset$ it follows that $U_n(x_n)\cap U_m(x_m)\neq\emptyset$ and so $x_n = x_m$ or $1 < |x_n-x_m|\leq \sqrt{2}$. But as $[-\sqrt{2}+x_1, \sqrt{2}+x_1]$ is totally bounded, the set $\{x_n : n\in\mathbb{N}\}$ must be finite, and so there is $x\in\mathbb{R}$ such that $x_n = x$ for infinitely many $x$. If $F\in\mathcal{F}$, then $U_n(x)\cap F\supseteq F_n\cap F\neq\emptyset$ for infinitely many $n$, and so $U_n(x)\cap F\neq\emptyset$ for all $n$, which implies $(x, 0)\in F$ for all $F\in\mathcal{F}$ or in other words $(x, 0)\in\bigcap\mathcal{F}$. diff --git a/spaces/S000215/properties/P000105.md b/spaces/S000215/properties/P000105.md new file mode 100644 index 0000000000..3bfa720228 --- /dev/null +++ b/spaces/S000215/properties/P000105.md @@ -0,0 +1,7 @@ +--- +space: S000215 +property: P000105 +value: false +--- + +Let $\mathcal{U} = \{U_1(x) : x\in\mathbb{R}\} \cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_1(x)\}$. If $X$ is para-Lindelof, then by taking a locally countable open refinement of $\mathcal{U}$, for every $x\in \mathbb{R}$ there is $n(x)\in\mathbb{N}$ such that $\{U_{n(x)}(x): x\in \mathbb{R}\}$ is locally countable. Find $n$ such that $n = n(x)$ for uncountably many $x\in\mathbb{R}$, and let $C = \{y\in\mathbb{R} : n = n(x)\}$. Take a two-sided condensation point $x$ of $C$ (citation needed!) and $m$ such that $U_m(x)$ intersects countably many $U_n(y)$ for $y\in C$. Note that there is $z < x$ such that $U_n(y)\cap U_m(x)\neq \emptyset$ for all $y\in (z, x)\cap C$, and since $(z, x)\cap C$ is uncountable we obtain a contradiction. From cd0ae058db714d68578910fcfb5f887c040d319b Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Tue, 9 Sep 2025 07:55:38 +0200 Subject: [PATCH 17/19] add brian scott great reference --- spaces/S000215/properties/P000105.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/spaces/S000215/properties/P000105.md b/spaces/S000215/properties/P000105.md index 3bfa720228..18db3b7851 100644 --- a/spaces/S000215/properties/P000105.md +++ b/spaces/S000215/properties/P000105.md @@ -2,6 +2,9 @@ space: S000215 property: P000105 value: false +refs: + - mathse: 412625 + name: Answer to "Every bounded non countable subset of $\mathbb{R}$ has a two-sided accumulation point." --- -Let $\mathcal{U} = \{U_1(x) : x\in\mathbb{R}\} \cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_1(x)\}$. If $X$ is para-Lindelof, then by taking a locally countable open refinement of $\mathcal{U}$, for every $x\in \mathbb{R}$ there is $n(x)\in\mathbb{N}$ such that $\{U_{n(x)}(x): x\in \mathbb{R}\}$ is locally countable. Find $n$ such that $n = n(x)$ for uncountably many $x\in\mathbb{R}$, and let $C = \{y\in\mathbb{R} : n = n(x)\}$. Take a two-sided condensation point $x$ of $C$ (citation needed!) and $m$ such that $U_m(x)$ intersects countably many $U_n(y)$ for $y\in C$. Note that there is $z < x$ such that $U_n(y)\cap U_m(x)\neq \emptyset$ for all $y\in (z, x)\cap C$, and since $(z, x)\cap C$ is uncountable we obtain a contradiction. +Let $\mathcal{U} = \{U_1(x) : x\in\mathbb{R}\} \cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_1(x)\}$. If $X$ is para-Lindelof, then by taking a locally countable open refinement of $\mathcal{U}$, for every $x\in \mathbb{R}$ there is $n(x)\in\mathbb{N}$ such that $\{U_{n(x)}(x): x\in \mathbb{R}\}$ is locally countable. Find $n$ such that $n = n(x)$ for uncountably many $x\in\mathbb{R}$, and let $C = \{y\in\mathbb{R} : n = n(x)\}$. Take a point $x$ of $C$ such that for any $y < x < z$ the sets $(y, x)\cap C$ and $(x, z)\cap C$ are uncountable (see {{mathse:412625}} for proof that such point exists), and $m$ such that $U_m(x)$ intersects countably many $U_n(y)$ for $y\in C$. Note that there is $z < x$ such that $U_n(y)\cap U_m(x)\neq \emptyset$ for all $y\in (z, x)\cap C$, and since $(z, x)\cap C$ is uncountable we obtain a contradiction. From f1177425055b435c7c3d8615ccb00629a3886597 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Tue, 9 Sep 2025 12:14:24 +0200 Subject: [PATCH 18/19] added S133, added locally orderable --- spaces/S000215/properties/P000022.md | 5 +---- spaces/S000215/properties/P000023.md | 7 ------- spaces/S000215/properties/P000082.md | 2 +- spaces/S000215/properties/P000093.md | 2 +- spaces/S000215/properties/P000120.md | 7 +++++++ spaces/S000215/properties/P000130.md | 7 +++++++ spaces/S000215/properties/P000198.md | 2 +- 7 files changed, 18 insertions(+), 14 deletions(-) delete mode 100644 spaces/S000215/properties/P000023.md create mode 100644 spaces/S000215/properties/P000120.md create mode 100644 spaces/S000215/properties/P000130.md diff --git a/spaces/S000215/properties/P000022.md b/spaces/S000215/properties/P000022.md index bd4b24a164..7537efe4c5 100644 --- a/spaces/S000215/properties/P000022.md +++ b/spaces/S000215/properties/P000022.md @@ -2,9 +2,6 @@ space: S000215 property: P000022 value: false -refs: - - mathse: 4718866 - name: Mysior plane is not realcompact --- -The function $f:X\to\mathbb{R}$ defined by $f(x, y) = \begin{cases} x, & y = 1 \\ 0, & y\neq 1 \end{cases}$ is continuous and unbounded. +$U_1(x)$ is clopen and homeomorphic to {S133} and {S133|P22}. diff --git a/spaces/S000215/properties/P000023.md b/spaces/S000215/properties/P000023.md deleted file mode 100644 index e7d74624d7..0000000000 --- a/spaces/S000215/properties/P000023.md +++ /dev/null @@ -1,7 +0,0 @@ ---- -space: S000215 -property: P000023 -value: false ---- - -If $V$ is a compact neighbourhood of $(x, 0)$, then $U_n(x)\subseteq V$ for some $n$. Since $U_n(x)$ is closed, it follows that it must be compact. But since $U_{n+1}(x)\setminus U_n(x)$ is a discrete open set of size $\mathfrak{c}$, the family $\mathcal{U} = \{U_{n+1}(x)\} \cup \{\{y\}: y\in U_n(x)\setminus U_{n+1}(x) \}$ is an open partition of $U_n(x)$ without a finite subcover. diff --git a/spaces/S000215/properties/P000082.md b/spaces/S000215/properties/P000082.md index 5d1a1dd821..20d5f96f7a 100644 --- a/spaces/S000215/properties/P000082.md +++ b/spaces/S000215/properties/P000082.md @@ -4,4 +4,4 @@ property: P000082 value: true --- -If $(x, y)\in X$ and $y\neq 0$, then $(x, y)$ is isolated and so has a metrizable neighbourhood. If $y = 0$ then from {T643} the neighourhood $U_n(x)$ of $(x, y)$ is metrizable. +$U_1(x)$ is homeomorphic to {S133} and {S133|P53} diff --git a/spaces/S000215/properties/P000093.md b/spaces/S000215/properties/P000093.md index e4b9dc3f19..11b75574dd 100644 --- a/spaces/S000215/properties/P000093.md +++ b/spaces/S000215/properties/P000093.md @@ -4,4 +4,4 @@ property: P000093 value: false --- -The neighbourhoods $U_n(x)$ of $(x, 0)$ are uncountable. +$U_n(x)$ is homeomorphic to {S133} and {S133|P57}. diff --git a/spaces/S000215/properties/P000120.md b/spaces/S000215/properties/P000120.md new file mode 100644 index 0000000000..73ed97c5c6 --- /dev/null +++ b/spaces/S000215/properties/P000120.md @@ -0,0 +1,7 @@ +--- +space: S000215 +property: P000120 +value: true +--- + +$U_1(x)$ is homeomorphic to {S133} and {S133|P133}. diff --git a/spaces/S000215/properties/P000130.md b/spaces/S000215/properties/P000130.md new file mode 100644 index 0000000000..0b1f8e4e4a --- /dev/null +++ b/spaces/S000215/properties/P000130.md @@ -0,0 +1,7 @@ +--- +space: S000215 +property: P000130 +value: false +--- + +$U_n(x)$ is homeomorphic to {S133} and {S133|P130} diff --git a/spaces/S000215/properties/P000198.md b/spaces/S000215/properties/P000198.md index 348cb862d7..2d7e5b5688 100644 --- a/spaces/S000215/properties/P000198.md +++ b/spaces/S000215/properties/P000198.md @@ -4,4 +4,4 @@ property: P000198 value: false --- -$\mathbb{R}\times [1, \infty)$ is an uncountable closed discrete subset of $X$ +$\mathbb{R}\times \{0\}$ is an uncountable closed discrete subset of $X$ From 42051511f0052639e3c3e757cae92f22cc8eccc7 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Tue, 16 Dec 2025 20:15:37 +0100 Subject: [PATCH 19/19] remove P82 --- spaces/S000215/properties/P000082.md | 7 ------- 1 file changed, 7 deletions(-) delete mode 100644 spaces/S000215/properties/P000082.md diff --git a/spaces/S000215/properties/P000082.md b/spaces/S000215/properties/P000082.md deleted file mode 100644 index 20d5f96f7a..0000000000 --- a/spaces/S000215/properties/P000082.md +++ /dev/null @@ -1,7 +0,0 @@ ---- -space: S000215 -property: P000082 -value: true ---- - -$U_1(x)$ is homeomorphic to {S133} and {S133|P53}