From 58287b09142aed592b74b52adb2334da9318ce87 Mon Sep 17 00:00:00 2001 From: Batixx Date: Sun, 17 May 2026 04:38:30 +0200 Subject: [PATCH 1/4] Countable + P space => Alexandrov --- properties/P000090.md | 1 + theorems/T000894.md | 14 ++++++++++++++ 2 files changed, 15 insertions(+) create mode 100644 theorems/T000894.md diff --git a/properties/P000090.md b/properties/P000090.md index 511f5d1a62..391805ba93 100644 --- a/properties/P000090.md +++ b/properties/P000090.md @@ -17,6 +17,7 @@ This is equivalent to each of the following: * An arbitrary union of closed sets is closed. * Each $x \in X$ has a smallest neighborhood. +* For each $x \in X$, the *neighborhood kernel of $x$*, i. e. $\bigcap\big\{U\text{ open in }X\mid x\in U\big\}$, is open. * $X$ is *finitely generated*: For each $A \subseteq X$, $A$ is open iff $A \cap Y$ is open in the subspace $Y$ for each finite $Y \subseteq X$. * There is a preorder (i.e., a reflexive and transitive relation) $\preceq$ on $X$ such that the open sets are precisely the upward closed sets (i.e., sets $A\subseteq X$ such that $x\in A$ and $x\preceq y$ imply $y\in A$). diff --git a/theorems/T000894.md b/theorems/T000894.md new file mode 100644 index 0000000000..2291009648 --- /dev/null +++ b/theorems/T000894.md @@ -0,0 +1,14 @@ +--- +uid: T000894 +if: + and: + - P000057: true + - P000147: true +then: + P000090: true +--- + +Let $x \in X$ and $A$ the neighborhood kernel of $x$. + +For every $y \not\in A$ we find an open neighborhood $U_y$ of $x$ not containing $y$. +Since $X$ is countable, so is $S := \{U_y\mid y \not\in A\}$. By {P147}, this implies $\bigcap S = A$ is open, which implies the assertion. From 36b4cdc8d0746b465b262b435bf9a8f4b39298a8 Mon Sep 17 00:00:00 2001 From: Batixx Date: Sun, 17 May 2026 04:41:21 +0200 Subject: [PATCH 2/4] missing be --- theorems/T000894.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theorems/T000894.md b/theorems/T000894.md index 2291009648..7dcaad0f79 100644 --- a/theorems/T000894.md +++ b/theorems/T000894.md @@ -8,7 +8,7 @@ then: P000090: true --- -Let $x \in X$ and $A$ the neighborhood kernel of $x$. +Let $x \in X$ and $A$ be the neighborhood kernel of $x$. For every $y \not\in A$ we find an open neighborhood $U_y$ of $x$ not containing $y$. Since $X$ is countable, so is $S := \{U_y\mid y \not\in A\}$. By {P147}, this implies $\bigcap S = A$ is open, which implies the assertion. From 1f3c1e841629112b01722896e1c77b9426b1ce7f Mon Sep 17 00:00:00 2001 From: Batixx Date: Sun, 17 May 2026 06:14:08 +0200 Subject: [PATCH 3/4] adapt for locally countable --- theorems/T000894.md | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/theorems/T000894.md b/theorems/T000894.md index 7dcaad0f79..7798aab0d5 100644 --- a/theorems/T000894.md +++ b/theorems/T000894.md @@ -2,13 +2,14 @@ uid: T000894 if: and: - - P000057: true + - P000093: true - P000147: true then: P000090: true --- -Let $x \in X$ and $A$ be the neighborhood kernel of $x$. +Let $x \in X$, $A$ be the neighborhood kernel of $x$ and, by {P93}, $V$ be a countable open neighborhood of $x$. -For every $y \not\in A$ we find an open neighborhood $U_y$ of $x$ not containing $y$. -Since $X$ is countable, so is $S := \{U_y\mid y \not\in A\}$. By {P147}, this implies $\bigcap S = A$ is open, which implies the assertion. +If $V=A$ we are clearly done. +Otherwise, we find for every $y \in V \setminus A$ an open neighborhood $U_y\subseteq V$ of $x$ not containing $y$. +Since $X$ is countable, so is $S := \{U_y\mid y \in V \setminus A\}$. By {P147}, this implies $\bigcap S = A$ is open, which implies the assertion. From 972568d47cfe284293d761e0dc7878e8e53e489e Mon Sep 17 00:00:00 2001 From: Felix Pernegger Date: Mon, 18 May 2026 00:19:16 +0200 Subject: [PATCH 4/4] Update theorems/T000894.md Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> --- theorems/T000894.md | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/theorems/T000894.md b/theorems/T000894.md index 7798aab0d5..27f64dcecf 100644 --- a/theorems/T000894.md +++ b/theorems/T000894.md @@ -8,8 +8,11 @@ then: P000090: true --- -Let $x \in X$, $A$ be the neighborhood kernel of $x$ and, by {P93}, $V$ be a countable open neighborhood of $x$. +Let $x \in X$ and let $A=\bigcap\{U\text{ open in }X: x\in U\}$ be the neighborhood kernel of $x$. +We need to show that $A$ is open in $X$. -If $V=A$ we are clearly done. -Otherwise, we find for every $y \in V \setminus A$ an open neighborhood $U_y\subseteq V$ of $x$ not containing $y$. -Since $X$ is countable, so is $S := \{U_y\mid y \in V \setminus A\}$. By {P147}, this implies $\bigcap S = A$ is open, which implies the assertion. +Take a countable open neighborhood $V$ of $x$. +For each $y\in V\setminus A$ there is an open neighborhood $U_y$ of $x$ not containing $y$. +Since $V$ is countable, the countable intersection +$V\cap\bigcap\{U_y: y\in V\setminus A\}$ is open by {P147}. +And that intersection is equal to $A$.