Pseudometricised function spaces.

src/topology/functions/set-systems.tex

@@ -46,7 +46,8 @@
         \[
         E(T, U \cap U') \subset E(S \cup S', U \cap U') \subset E(S, U) \cap E(S', U')
         \]
-        \item[(FB3)] For any $U \in \fU$, there exists $V \in \fV$ with $V \circ V \subset U$. Thus for any $S \in \mathfrak{S}$,
+        \item[(UB1)] For any $U \in \fU$, $\Delta \subset U$. Thus the diagonal in $X^T$ is in $E(S, U)$ for any $S \in \mathfrak{S}$.
+        \item[(UB2)] For any $U \in \fU$, there exists $V \in \fV$ with $V \circ V \subset U$. Thus for any $S \in \mathfrak{S}$,
         \[
         E(S, V) \circ E(S, V) \subset E(S, V \circ V) \subset E(S, U)
         \]
@@ -54,6 +55,44 @@
     By \ref{proposition:fundamental-entourage-criterion}, $\mathfrak{E}$ is a fundamental system of entourages for the uniformity that it generates.
 \end{proof}
 
+\begin{proposition}
+\label{proposition:set-uniform-pseudometric}
+    Let $T$ be a set, $\mathfrak{S} \subset 2^T$ be a non-empty family of sets, and $(X, \fU)$ be a uniform space whose uniformity is induced by the pseudometrics $\seqi{d}$. For each $i \in I$ and $S \in \mathfrak{S}$, let
+    \[
+    d_{i, S}: X^T \times X^T \quad (f, g) \mapsto \sup_{x \in S}d_i(f(x), g(x))
+    \]
+    then
+    \begin{enumerate}
+        \item $\bracs{d_{i, S}| i \in I, S \in \mathfrak{S}}$ is a family of pseudometrics induces the $\mathfrak{S}$-uniformity on $X^T$.
+        \item If $\mathfrak{S}$ is upward-directed with respect to inclusion, then
+        \[
+        \bracs{\bigcap_{j \in J}E(d_{j, S}, r)|J \subset I \text{ finite}, r > 0, S \in \mathfrak{S}}
+        \]
+        is a fundamental system of entourages for the $\mathfrak{S}$-uniformity on $X^T$.
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    (1): Let $S \in \mathfrak{S}$ and $U \in \fU$, then there exists $r > 0$ and $J \subset I$ finite such that $\bigcap_{j \in J}E(d_j, r) \subset U$, so
+    \[
+    \bigcap_{j \in J}E(d_{j, S}, r) \subset E\paren{S, \bigcap_{j \in J}E(d_j, r)} \subset E(S, U)
+    \]
+    and the uniformity induced by $\bracs{d_{i, S}| i \in I, S \in \mathfrak{S}}$ contains the $\mathfrak{S}$-uniformity.
+
+    On the other hand, for any $i \in I$ and $r > 0$, $E(d_j, r/2) \in \fU$ by \ref{definition:pseudometric-uniformity}. Therefore $E(S, E(d_j, r/2)) \subset E(d_{j, S}, r)$, so the $\mathfrak{S}$-uniformity contains the induced uniformity.
+
+    (2): If $\mathfrak{S}$ is upward-directed with respect to inclusion, then by \ref{definition:set-uniform},
+    \[
+    \bracs{E(S, U)| U \in \fU, S \in \mathfrak{S}}
+    \]
+    Following the same steps in (1),
+    \[
+    \bracs{\bigcap_{j \in J}E(d_{j, S}, r)|J \subset I \text{ finite}, r > 0, S \in \mathfrak{S}}
+    \]
+    is a fundamental system of entourages for the $\mathfrak{S}$-uniformity.
+\end{proof}
+
+
+
 \begin{definition}[Pointwise Topology]
 \label{definition:pointwise}
     Let $T$ be a set and $X$ be a topological space, then the following topologies on $X^T$ coincide: