jerrylicious/garden
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

MAJOR RETRACTION IN UNIFORMITY DEFINING PROPOSITION.

Browse Source
This commit is contained in:
Bokuan Li
2026-06-21 21:56:28 -04:00
parent a57686be8f
commit f107df48bf
8 changed files with 97 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/fa/tvs/definition.tex
View File

@@ -100,7 +100,7 @@
\begin{enumerate}
\item[(FB1)] For any $V, V' \in \fB$, there exists $W \in \fB$ with $W \subset V \cap V'$. In which case, $U_{V} \cap U_{V'} \supset U_W \in \mathfrak{V}$.
\item[(UB1)] For any $x \in E$ and $V \in \fB$, $x - x = 0 \in V$, so $\Delta \subset U_V$.
\item[(UB2)] For any $V \in \fB$, by (TVB1), there exists $W \in \fB$ such that $W + W \subset V$. In which case, for any $x, y, z \in E$ with $x - y, y - z \in W$, $x - z \in V$. Therefore $U_W \circ U_W \subset U_V$.
\item[(UB3)] For any $V \in \fB$, by (TVB1), there exists $W \in \fB$ such that $W + W \subset V$. In which case, for any $x, y, z \in E$ with $x - y, y - z \in W$, $x - z \in V$. Therefore $U_W \circ U_W \subset U_V$.
\end{enumerate}
By \autoref{proposition:fundamental-entourage-criterion}, there exists a unique uniformity $\fU$ on $E$ for which $\mathfrak{V}$ is a fundamental system of entourages.