From ce1499c094200fe00302cfcf591968eb2160977b Mon Sep 17 00:00:00 2001 From: Geoffrey Sangston Date: Sat, 18 Apr 2026 16:34:18 -0400 Subject: [PATCH 1/3] Euclidean line and plane --- spaces/S000025/properties/P000087.md | 7 ------- spaces/S000025/properties/P000238.md | 7 +++++++ spaces/S000176/properties/P000087.md | 7 ------- spaces/S000176/properties/P000199.md | 10 ---------- spaces/S000176/properties/P000238.md | 7 +++++++ 5 files changed, 14 insertions(+), 24 deletions(-) delete mode 100644 spaces/S000025/properties/P000087.md create mode 100644 spaces/S000025/properties/P000238.md delete mode 100644 spaces/S000176/properties/P000087.md delete mode 100644 spaces/S000176/properties/P000199.md create mode 100644 spaces/S000176/properties/P000238.md diff --git a/spaces/S000025/properties/P000087.md b/spaces/S000025/properties/P000087.md deleted file mode 100644 index 037a83bd35..0000000000 --- a/spaces/S000025/properties/P000087.md +++ /dev/null @@ -1,7 +0,0 @@ ---- -space: S000025 -property: P000087 -value: true ---- - -$(\mathbb R,+)$ is a topological group. diff --git a/spaces/S000025/properties/P000238.md b/spaces/S000025/properties/P000238.md new file mode 100644 index 0000000000..a4cb5a66b9 --- /dev/null +++ b/spaces/S000025/properties/P000238.md @@ -0,0 +1,7 @@ +--- +space: S000025 +property: P000238 +value: true +--- + +The standard addition and scalar multiplication on $\mathbb R$ are continuous, and together satisfy the axioms of a real vector space. diff --git a/spaces/S000176/properties/P000087.md b/spaces/S000176/properties/P000087.md deleted file mode 100644 index 03d1ea1c37..0000000000 --- a/spaces/S000176/properties/P000087.md +++ /dev/null @@ -1,7 +0,0 @@ ---- -space: S000176 -property: P000087 -value: true ---- - -$\mathbb{R}^2$ is a product of topological groups, namely $\mathbb{R}$. See {S25|P87}. diff --git a/spaces/S000176/properties/P000199.md b/spaces/S000176/properties/P000199.md deleted file mode 100644 index 9616686155..0000000000 --- a/spaces/S000176/properties/P000199.md +++ /dev/null @@ -1,10 +0,0 @@ ---- -space: S000176 -property: P000199 -value: true -refs: - - mathse: 4463999 - name: The cartesian product of contractible spaces is contractible ---- - -This follows because {S25|P199} and a product of contractible spaces is contractible. See {{mathse:4463999}}. diff --git a/spaces/S000176/properties/P000238.md b/spaces/S000176/properties/P000238.md new file mode 100644 index 0000000000..9e7989bbe2 --- /dev/null +++ b/spaces/S000176/properties/P000238.md @@ -0,0 +1,7 @@ +--- +space: S000176 +property: P000238 +value: true +--- + +Same argument as {S25|P238}. From 1feeb1216f62c8724c11bea612ec80c3d6b99f90 Mon Sep 17 00:00:00 2001 From: Geoffrey Sangston Date: Sat, 18 Apr 2026 16:41:56 -0400 Subject: [PATCH 2/3] separable hilbert space is tvs --- spaces/S000030/properties/P000087.md | 7 ------- spaces/S000030/properties/P000199.md | 7 ------- spaces/S000030/properties/P000238.md | 7 +++++++ 3 files changed, 7 insertions(+), 14 deletions(-) delete mode 100644 spaces/S000030/properties/P000087.md delete mode 100644 spaces/S000030/properties/P000199.md create mode 100644 spaces/S000030/properties/P000238.md diff --git a/spaces/S000030/properties/P000087.md b/spaces/S000030/properties/P000087.md deleted file mode 100644 index dfc88ad50d..0000000000 --- a/spaces/S000030/properties/P000087.md +++ /dev/null @@ -1,7 +0,0 @@ ---- -space: S000030 -property: P000087 -value: true ---- - -$\mathbb{R}^\omega$ is a product of topological groups, namely $\mathbb{R}$. See {S25|P87}. diff --git a/spaces/S000030/properties/P000199.md b/spaces/S000030/properties/P000199.md deleted file mode 100644 index 1a116d84ff..0000000000 --- a/spaces/S000030/properties/P000199.md +++ /dev/null @@ -1,7 +0,0 @@ ---- -space: S000030 -property: P000199 -value: true ---- - -This follows because $X$ has the structure of a topological vector space over the reals, so that there exists a straight line homotopy from the identity map to the constant map with value $0$. diff --git a/spaces/S000030/properties/P000238.md b/spaces/S000030/properties/P000238.md new file mode 100644 index 0000000000..bbd8ae5fa0 --- /dev/null +++ b/spaces/S000030/properties/P000238.md @@ -0,0 +1,7 @@ +--- +space: S000030 +property: P000238 +value: true +--- + +$\mathbb{R}^\omega$ is a product of topological vector spaces, namely $\mathbb{R}$. And {S25|P238}. From ad9f7b91e904f7193bf4253d861f9939b664c161 Mon Sep 17 00:00:00 2001 From: Geoffrey Sangston Date: Sun, 19 Apr 2026 09:10:40 -0400 Subject: [PATCH 3/3] Apply Felix's suggestion to type it out again --- spaces/S000176/properties/P000238.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spaces/S000176/properties/P000238.md b/spaces/S000176/properties/P000238.md index 9e7989bbe2..1dd5075896 100644 --- a/spaces/S000176/properties/P000238.md +++ b/spaces/S000176/properties/P000238.md @@ -4,4 +4,4 @@ property: P000238 value: true --- -Same argument as {S25|P238}. +The standard addition and scalar multiplication on $\mathbb R^2$ are continuous, and together satisfy the axioms of a real vector space.