From 1e970e195b5e9430dda4c1d10582a638b7b4c385 Mon Sep 17 00:00:00 2001 From: Batixx Date: Tue, 31 Mar 2026 01:08:56 +0200 Subject: [PATCH 1/5] s136 scattered --- spaces/S000136/properties/P000019.md | 3 --- spaces/S000136/properties/P000051.md | 9 +++++++++ spaces/S000136/properties/P000139.md | 10 ---------- spaces/S000137/properties/P000051.md | 7 +++++++ 4 files changed, 16 insertions(+), 13 deletions(-) create mode 100644 spaces/S000136/properties/P000051.md delete mode 100644 spaces/S000136/properties/P000139.md create mode 100644 spaces/S000137/properties/P000051.md diff --git a/spaces/S000136/properties/P000019.md b/spaces/S000136/properties/P000019.md index 28cff145e9..711c767895 100644 --- a/spaces/S000136/properties/P000019.md +++ b/spaces/S000136/properties/P000019.md @@ -2,9 +2,6 @@ space: S000136 property: P000019 value: false -refs: -- zb: "0386.54001" - name: Counterexamples in Topology --- Closed subspaces of {P19} spaces are {P19}, but the closed subspace {S137} of this space is not {P19}. diff --git a/spaces/S000136/properties/P000051.md b/spaces/S000136/properties/P000051.md new file mode 100644 index 0000000000..09aef72ce4 --- /dev/null +++ b/spaces/S000136/properties/P000051.md @@ -0,0 +1,9 @@ +--- +space: S000136 +property: P000051 +value: true +--- + +For $r \in \mathbb{R}$ consider the characteristic function $\chi_{\{r\}}:2^\mathbb{R}\to 2$. Then $\chi_{\{r\}} \cap M = x_r$, therefore $M$ is discrete as a subspace. + +Thus if $A \subseteq X$ contains no elements of $F$ we are done, otherwise $A$ already contains an isolated point by definition. diff --git a/spaces/S000136/properties/P000139.md b/spaces/S000136/properties/P000139.md deleted file mode 100644 index 7fc389e629..0000000000 --- a/spaces/S000136/properties/P000139.md +++ /dev/null @@ -1,10 +0,0 @@ ---- -space: S000136 -property: P000139 -value: true -refs: -- zb: "0386.54001" - name: Counterexamples in Topology ---- - -Every point in $X\setminus M$ is isolated by definition. diff --git a/spaces/S000137/properties/P000051.md b/spaces/S000137/properties/P000051.md new file mode 100644 index 0000000000..3b973da72e --- /dev/null +++ b/spaces/S000137/properties/P000051.md @@ -0,0 +1,7 @@ +--- +space: S000136 +property: P000051 +value: true +--- + +$X$ is a subspace of {S136} and {S136|P51}. From 96839c923f987f565f606717bec56de844297079 Mon Sep 17 00:00:00 2001 From: Batixx Date: Tue, 31 Mar 2026 01:09:57 +0200 Subject: [PATCH 2/5] wrong uid --- spaces/S000137/properties/P000051.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spaces/S000137/properties/P000051.md b/spaces/S000137/properties/P000051.md index 3b973da72e..051baf3622 100644 --- a/spaces/S000137/properties/P000051.md +++ b/spaces/S000137/properties/P000051.md @@ -1,5 +1,5 @@ --- -space: S000136 +space: S000137 property: P000051 value: true --- From 5d229dbb966a2b815a58a9825c20fc0af15632d0 Mon Sep 17 00:00:00 2001 From: Felix Pernegger Date: Fri, 15 May 2026 17:53:20 +0200 Subject: [PATCH 3/5] fix proof --- spaces/S000136/properties/P000051.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spaces/S000136/properties/P000051.md b/spaces/S000136/properties/P000051.md index 09aef72ce4..db87212525 100644 --- a/spaces/S000136/properties/P000051.md +++ b/spaces/S000136/properties/P000051.md @@ -4,6 +4,6 @@ property: P000051 value: true --- -For $r \in \mathbb{R}$ consider the characteristic function $\chi_{\{r\}}:2^\mathbb{R}\to 2$. Then $\chi_{\{r\}} \cap M = x_r$, therefore $M$ is discrete as a subspace. +For $r \in \mathbb{R}$ consider $U_r := \{f \in 2^\mathbb{R} \to 2\mid f(\{r\})=1\} \subseteq X$. Note $U_r$ is open in the product topology and therefore open in $X$. Furthermore $U_r \cap M = \{x_r\}$, so $x_r$ is isolated in $M$ and thus $M$ is discrete as a subspace. -Thus if $A \subseteq X$ contains no elements of $F$ we are done, otherwise $A$ already contains an isolated point by definition. +Hence, if $A \subseteq X$ contains no elements of $F$ we are done, otherwise $A$ already contains an isolated point by definition. From 46a7e6354c38e496426d1a03b60851fb8436a123 Mon Sep 17 00:00:00 2001 From: Felix Pernegger Date: Fri, 15 May 2026 17:55:30 +0200 Subject: [PATCH 4/5] insert missing word --- spaces/S000136/properties/P000051.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spaces/S000136/properties/P000051.md b/spaces/S000136/properties/P000051.md index db87212525..687b361cbb 100644 --- a/spaces/S000136/properties/P000051.md +++ b/spaces/S000136/properties/P000051.md @@ -4,6 +4,6 @@ property: P000051 value: true --- -For $r \in \mathbb{R}$ consider $U_r := \{f \in 2^\mathbb{R} \to 2\mid f(\{r\})=1\} \subseteq X$. Note $U_r$ is open in the product topology and therefore open in $X$. Furthermore $U_r \cap M = \{x_r\}$, so $x_r$ is isolated in $M$ and thus $M$ is discrete as a subspace. +For $r \in \mathbb{R}$ consider $U_r := \{f \in 2^\mathbb{R} \to 2\mid f(\{r\})=1\} \subseteq X$. Note that $U_r$ is open in the product topology and therefore open in $X$. Furthermore $U_r \cap M = \{x_r\}$, so $x_r$ is isolated in $M$ and thus $M$ is discrete as a subspace. Hence, if $A \subseteq X$ contains no elements of $F$ we are done, otherwise $A$ already contains an isolated point by definition. From b0f24085a034166c529e014bad63f0fae7f34ea3 Mon Sep 17 00:00:00 2001 From: Felix Pernegger Date: Fri, 15 May 2026 17:57:13 +0200 Subject: [PATCH 5/5] one more typo --- spaces/S000136/properties/P000051.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spaces/S000136/properties/P000051.md b/spaces/S000136/properties/P000051.md index 687b361cbb..5dcb169b0a 100644 --- a/spaces/S000136/properties/P000051.md +++ b/spaces/S000136/properties/P000051.md @@ -6,4 +6,4 @@ value: true For $r \in \mathbb{R}$ consider $U_r := \{f \in 2^\mathbb{R} \to 2\mid f(\{r\})=1\} \subseteq X$. Note that $U_r$ is open in the product topology and therefore open in $X$. Furthermore $U_r \cap M = \{x_r\}$, so $x_r$ is isolated in $M$ and thus $M$ is discrete as a subspace. -Hence, if $A \subseteq X$ contains no elements of $F$ we are done, otherwise $A$ already contains an isolated point by definition. +Hence, if $A \subseteq X$ contains no elements of $X \setminus M$ we are done, otherwise $A$ already contains an isolated point by definition.