Added the Mackey-Arens theorem.

src/dg/complex/runge.tex

@@ -16,7 +16,7 @@
     \end{enumerate}
 \end{proposition}
 \begin{proof}[Proof, {{\cite[Proposition VIII.1.1]{ConwayComplex}}}. ]
-    Via \hyperref[fattening]{proposition:distance-compact}, let $V \in \cn_\complex^o(K)$ precompact with $\ol V \subset U$. Identify $\complex = \real^2$, then since $V$ is precompact, there exists $\delta > 0$ and $\seqf{(x_j, y_j)} \subset U$ such that:
+    Via \hyperref[fattening]{proposition:distance-compact}, let $V \in \cn_\complex^o(K)$ relatively compact with $\ol V \subset U$. Identify $\complex = \real^2$, then since $V$ is relatively compact, there exists $\delta > 0$ and $\seqf{(x_j, y_j)} \subset U$ such that:
     \begin{enumerate}
         \item For each $1 \le j \le n$, $R_j = [x_j, x_j + \delta] \times [y_j, y_j + \delta] \subset U$. 
         \item $\bigcup_{j = 1}^n R_j \supset V$. 

src/dg/complex/space.tex

@@ -24,8 +24,8 @@
 
     and the following are equivalent:
     \begin{enumerate}[label=(C\arabic*)]
-        \item $\cf$ is precompact in $H(U; E)$. 
+        \item $\cf$ is relatively compact in $H(U; E)$. 
-        \item $\cf$ is bounded in $H(U; E)$, and for each $x \in U$, $\cf(x) = \bracs{f(x)|f \in \cf}$ is precompact.  
+        \item $\cf$ is bounded in $H(U; E)$, and for each $x \in U$, $\cf(x) = \bracs{f(x)|f \in \cf}$ is relatively compact.  
     \end{enumerate}
 \end{theorem}
 \begin{proof}

src/dg/derivative/sets.tex

@@ -43,7 +43,7 @@
 
 \begin{definition}
 \label{definition:derivative-garden}
-    Let $E, F$ be TVSs over $K \in \RC$ with $F$ being separated, $\sigma^E_{\text{Fin}}, \sigma^E_{c}, \sigma^E_b \subset 2^E$ be the collection of all finite, precompact, and bounded subsets, respectively, then differentiability with respect to $\sigma^E_{\text{Fin}}, \sigma^E_{c}, \sigma^E_b$ correspond to \textbf{Gateaux}, \textbf{Hadamard}, and \textbf{Fréchet} differentiability.
+    Let $E, F$ be TVSs over $K \in \RC$ with $F$ being separated, $\sigma^E_{\text{Fin}}, \sigma^E_{c}, \sigma^E_b \subset 2^E$ be the collection of all finite, relatively compact, and bounded subsets, respectively, then differentiability with respect to $\sigma^E_{\text{Fin}}, \sigma^E_{c}, \sigma^E_b$ correspond to \textbf{Gateaux}, \textbf{Hadamard}, and \textbf{Fréchet} differentiability.
 \end{definition}
 
 
@@ -84,7 +84,7 @@
 \label{proposition:chain-rule-sets-conditions}
     Let $E$, $F$, $G$, be TVSs over $K \in \RC$ with $F, G$ being separated. If $\sigma \subset \mathfrak{B}(E)$ and $\tau \subset \mathfrak{B}(F)$ correspond to the following families of sets on $E$ and $F$:
     \begin{enumerate}
-        \item Precompact sets.
+        \item Relatively compact sets.
         \item Bounded sets.
     \end{enumerate}
 

src/fa/duality/mackey.tex

@@ -0,0 +1,68 @@
+\section{The Mackey-Arens Theorem}
+\label{section:mackey-arens}
+
+\begin{definition}[Consistent]
+\label{definition:consistent-lct-dual}
+    Let $\dpn{E, F}{\lambda}$ be a duality over $K \in \RC$ and $\mathcal{T} \subset 2^E$ be a locally convex topology, then $\mathcal{T}$ is \textbf{consistent} with $\dpn{E, F}{\lambda}$ if $(E, \mathcal{T})^* = F$. 
+\end{definition}
+
+\begin{lemma}
+\label{lemma:consistent-same-convex}
+    Let $\dpn{E, F}{\lambda}$ be a duality over $K \in \RC$, $\mathcal{T} \subset 2^E$ be a locally convex topology consistent with $\dpn{E, F}{\lambda}$, then for any $A \subset E$ convex, the $\mathcal{T}$-closure of $A$ and the $\sigma(E, F)$-closure of $A$ coincide. 
+\end{lemma}
+\begin{proof}
+    By the \hyperref[Hahn-Banach theorem]{theorem:hahn-banach-geometric-2}. 
+\end{proof}
+
+
+\begin{theorem}[Mackey-Arens]
+\label{theorem:mackey-arens}
+    Let $\dpn{E, F}{\lambda}$ be a duality over $K \in \RC$. 
+    \begin{enumerate}
+        \item[(E)] For any locally convex topology $\mathcal{T} \subset 2^E$ consistent with $\dpn{E, F}{\lambda}$, $\mathcal{T}$ is the topology of uniform convergence on all $\mathcal{T}$-equicontinuous subsets of $F$. 
+        \item[(C)] For any saturated covering ideal $\sigma \subset 2^{F}$ consisting of relatively $\sigma(F, E)$-compact sets, the $\sigma$-uniform topology on $E$ is consistent with $\dpn{E, F}{\lambda}$. 
+    \end{enumerate}
+
+    Moreover, 
+    \begin{enumerate}
+        \item[(M)] The topology of uniform convergence on relatively $\sigma(F, E)$-compact, convex, and circled sets is the finest locally convex topology on $E$ consistent with $\dpn{E, F}{\lambda}$. 
+    \end{enumerate}
+
+    and strongest locally convex topology on $E$ consistent with $\dpn{E, F}{\lambda}$ is the \textbf{Mackey topology} of $\dpn{E, F}{\lambda}$ on $E$, denoted $\tau(E, F)$. 
+\end{theorem}
+\begin{proof}
+    (E): Let $\cf \subset F$ be a $\mathcal{T}$-equicontinuous subset, then $\cf^\circ \in \cn_{\mathcal{T}}(0)$. If $\cf$ is circled, then
+    \[
+    \cf^\circ = \bracsn{x \in E|\ |\dpn{x, y}{\lambda}| \le 1 \forall y \in \cf}
+    \]
+
+    Thus $\mathcal{T}$ is finer than the topology of uniform convergence on all $\mathcal{T}$-equicontinuous subsets of $F$. 
+    
+    Conversely, for any convex and closed neighbourhood $U \in \cn_{\mathcal{T}}(0)$, $U^\circ$ is equicontinuous. By the \hyperref[Bipolar Theorem]{theorem:bipolar}, $U^{\circ \circ} = U$, so the family
+    \[
+    \fB = \bracsn{\cf^\circ| \cf \subset F, \cf \text{ is } \mathcal{T}\text{-equicontinuous}}
+    \]
+
+    is a fundamental system of neighbourhoods at $0$ for $\mathcal{T}$. Hence $\mathcal{T}$ is coarser than the topology of uniform convergence on all $\mathcal{T}$-equicontinuous subsets of $F$. 
+
+    (C): Let $\mathcal{T}$ be the $\sigma$-uniform topology on $E$, and $E^*$ be the dual of $(E, \mathcal{T})$. Since $\sigma$ is covering, it contains all singletons, so $\mathcal{T} \supset \sigma(E, F)$, and $F \subset E^*$. Thus it is sufficient to show that $F = E^*$. 
+
+    Let $\phi \in E^*$ and $\bracs{\phi}^\circ$ be the polar of $\phi$ with respect to $\dpn{E, E^*}{E}$. Since $\phi$ is continuous, $\bracs{\phi}^\circ \in \cn_{\mathcal{T}}(0)$. Thus there exists $A \in \sigma$ and $\mu > 0$ such that
+    \[
+    \bracsn{x \in E|\dpn{x, \psi}{E} \le \mu \forall \psi \in A} \subset \bracsn{x \in E|\dpn{x, \phi}{E} \le 1} = \bracs{\phi}^\circ
+    \]
+
+    Since $\sigma$ is saturated, assume without loss of generality that $\mu = 1$ and that $A$ is convex, circled, and $\sigma(F, E)$-compact. In which case, let $A^\circ$ be the polar of $A$ with respect to $\dpn{E, E^*}{E}$, then
+    \[
+    A^\circ = \bracsn{x \in E|\dpn{x, \psi}{E} \le 1 \forall \psi \in A} \subset \bracs{\phi}^\circ
+    \]
+
+    Let $A^{\circ\circ}$ and $\bracs{\phi}^{\circ\circ}$ be the bipolar of $A$ and $\bracs{\phi}$ with respect to $\dpn{E, E^*}{E}$, then by \autoref{proposition:polar-gymnastics}, $A^{\circ\circ} \supset \bracs{\phi}^{\circ\circ}$. 
+
+    Now, $A$ is $\sigma(F, E)$-compact, and hence $\sigma(E^*, E)$-compact in $E^*$\footnote{Closedness is insufficient because $F$ is $\sigma(E^*, E)$-dense in $E^*$ by \autoref{lemma:duality-dense}. } by \autoref{proposition:compact-closed}. Thus by the \hyperref[Bipolar Theorem]{theorem:bipolar}, $\phi \in A^{\circ\circ} = A \subset F$. 
+
+    (M): By (C), the topology of uniform convergence on relatively $\sigma(E, F)$-compact, convex, and circled sets is consistent with $\dpn{E, F}{\lambda}$. 
+    
+    On the other hand, let $\mathcal{T} \subset 2^E$ be a locally convex topology consistent with $\dpn{E, F}{\lambda}$. By the \hyperref[Banach-Alaoglu Theorem]{theorem:alaoglu}, every $\mathcal{T}$-equicontinuous set is relatively $\sigma(F, E)$-compact. Therefore $\mathcal{T}$ is coarser than the topology of uniform convergence on relatively $\sigma(E, F)$-compact, convex, and circled sets. 
+\end{proof}
+

src/fa/duality/polar.tex

@@ -127,3 +127,15 @@
     Therefore $y \in A^{\circ}$, but $\text{Re}\dpn{x_0, y}{\lambda} > 1$, so $x_0 \not\in A^{\circ\circ}$.
 \end{proof}
 
+\begin{proposition}
+\label{proposition:polar-equicontinuous}
+    Let $E$ be a locally convex space, then:
+    \begin{enumerate}
+        \item For each equicontinuous family $\cf \subset E^*$ equicontinuous, $\cf^\circ \in \cn_E(0)$. 
+        \item For each $U \in \cn_E(0)$, $U^\circ$ is equicontinuous. 
+    \end{enumerate}
+\end{proposition}
+
+
+
+

src/fa/tvs/equicontinuous.tex

@@ -113,10 +113,10 @@
 % TODO: Replace this with a more general version involving polars in the future. 
 \begin{theorem}[Banach-Alaoglu]
 \label{theorem:alaoglu}
-    Let $E$ be a locally convex space over $K \in \RC$ and $\alg \subset E^*$ be equicontinuous, then $\alg$ is precompact with respect to $\sigma(E^*, E)$.
+    Let $E$ be a locally convex space over $K \in \RC$ and $\alg \subset E^*$ be equicontinuous, then $\alg$ is relatively compact with respect to $\sigma(E^*, E)$.
 \end{theorem}
 \begin{proof}
-    For each $x \in E$, $\alg(x) = \bracsn{\dpn{x, \phi}{E}|\phi \in \alg}$ is precompact by \autoref{proposition:equicontinuous-bounded}. By the \hyperref[Arzelà-Ascoli Theorem]{theorem:arzela-ascoli}, 
+    For each $x \in E$, $\alg(x) = \bracsn{\dpn{x, \phi}{E}|\phi \in \alg}$ is relatively compact by \autoref{proposition:equicontinuous-bounded}. By the \hyperref[Arzelà-Ascoli Theorem]{theorem:arzela-ascoli}, 
     \begin{enumerate}
         \item[(C2)] The $\sigma(E^*, E)$-closure of $\alg$ in $\prod_{x \in E}K$ is equicontinuous. 
         \item[(C3)] The $\sigma(E^*, E)$-closure of $\alg$ in $\prod_{x \in E}K$ is compact. 

src/measure/lcg/haar.tex

@@ -117,7 +117,7 @@
     \frac{1}{(h: f)} = \frac{(f: g)}{(h: f)(f: g)} \le I_g(f) \le \frac{(f: h)(h: g)}{(h: g)} = (f: h)
     \]
 
-    Thus $\mathcal{I}(f) = \bracs{I_g(f)|g \in C_c^+(G) \setminus \bracs{0}}$ is precompact for each $f \in C_c^+(G)$. 
+    Thus $\mathcal{I}(f) = \bracs{I_g(f)|g \in C_c^+(G) \setminus \bracs{0}}$ is relatively compact for each $f \in C_c^+(G)$. 
 
     For each $V \in \cn_G(1)$, let $E_V = \bracs{I_g|g \in C_c^+(V) \setminus \bracs{0}}$, then $\fF = \bracs{E_V|V \in \cn_G(1)}$ is a filter on the product space $\prod_{f \in C_c^+(G)}\ol{\mathcal{I}(f)}$. By \hyperref[Tychonoff's Theorem]{theorem:tychonoff}, $\prod_{f \in C_c^+(G)}\ol{\mathcal{I}(f)}$ is compact, and $\bigcap_{V \in \cn_G(1)}\ol{E_V} \ne \emptyset$. 
 

src/topology/functions/set-systems.tex

@@ -138,7 +138,7 @@
 
 \begin{proposition}
 \label{proposition:compact-uniform-open}
-    Let $X$ be a topological space, $\kappa \subset 2^X$ be the collection of all precompact sets in $X$, and $(Y, \fU)$ be a uniform space, then the $\kappa$-open topology and $\kappa$-uniform topology on $C(X; Y)$ coincide. 
+    Let $X$ be a topological space, $\kappa \subset 2^X$ be the collection of all relatively compact sets in $X$, and $(Y, \fU)$ be a uniform space, then the $\kappa$-open topology and $\kappa$-uniform topology on $C(X; Y)$ coincide. 
 \end{proposition}
 \begin{proof}
     By \autoref{definition:set-uniform}, the $\kappa$-uniform topology is finer than the $\kappa$-open topology. 

src/topology/main/baire.tex

@@ -51,7 +51,7 @@
     \end{enumerate}
 \end{theorem}
 \begin{proof}
-    Let $U \subset X$ be open and $\seq{U_n} \subset 2^X$ be open and dense. Let $V_0 = U$. For each $n \in \natp$, by density of $U_n$, there exists $x \in U_n \cap V_{n - 1}$. Since $X$ is regular (\autoref{definition:uniform-separated}/\autoref{proposition:compact-hausdorff-normal}), there exists $V_{n} \in \cn^o(x)$ such that $x \in V_{n} \subset \ol U_{n} \subset U_n \cap V_{n-1}$. If $X$ is locally compact, choose $V_n$ to be precompact. If $X$ is completely metrisable, choose $V_n$ such that $\text{diam}(V_n) \le 1/n$.
+    Let $U \subset X$ be open and $\seq{U_n} \subset 2^X$ be open and dense. Let $V_0 = U$. For each $n \in \natp$, by density of $U_n$, there exists $x \in U_n \cap V_{n - 1}$. Since $X$ is regular (\autoref{definition:uniform-separated}/\autoref{proposition:compact-hausdorff-normal}), there exists $V_{n} \in \cn^o(x)$ such that $x \in V_{n} \subset \ol U_{n} \subset U_n \cap V_{n-1}$. If $X$ is locally compact, choose $V_n$ to be relatively compact. If $X$ is completely metrisable, choose $V_n$ such that $\text{diam}(V_n) \le 1/n$.
 
     Now, if $X$ is locally compact, then by the finite intersection property, $\bigcap_{n \in \natp}\ol{V_n} \ne \emptyset$. If $X$ is completely metrisable, then $\seq{V_n}$ is a Cauchy filter base, and converges to at least one point, so $\bigcap_{n \in \natp}\ol{V_n} \ne \emptyset$.
 

src/topology/main/c0.tex

@@ -54,7 +54,7 @@ For details regarding the complex-valued cased, in particular its properties as
 \begin{proof}
     Let $\phi \in C_0(X; E)$. Using \autoref{proposition:c0-properties}, assume without loss of generality that $\phi \in C_c(X; E)$. 
 
-    Since $\supp{\phi}$ is compact, so is $\phi(X)$ by \autoref{proposition:compact-extensions}. Let $U \in \cn_E^o(0)$ be balanced, then there exists $\seqf{y_j} \subset E \setminus \bracs{0}$ such that $\bigcup_{j = 1}^n (y_j + U) \supset \phi(X)$. For each $1 \le j \le n$, let $V_j = \phi^{-1}(y_j + U)$, then $\seqf{V_j}$ is an open cover of $\supp{\phi}$ consisting of precompact open sets. By \autoref{proposition:lch-partition-of-unity}, there exists a partition of unity $\seqf{\phi_j} \subset C_c(X; [0, 1])$ on $\supp{\phi}$ subordinate to $\seqf{V_j}$. For any $x \in E$, 
+    Since $\supp{\phi}$ is compact, so is $\phi(X)$ by \autoref{proposition:compact-extensions}. Let $U \in \cn_E^o(0)$ be balanced, then there exists $\seqf{y_j} \subset E \setminus \bracs{0}$ such that $\bigcup_{j = 1}^n (y_j + U) \supset \phi(X)$. For each $1 \le j \le n$, let $V_j = \phi^{-1}(y_j + U)$, then $\seqf{V_j}$ is an open cover of $\supp{\phi}$ consisting of relatively compact open sets. By \autoref{proposition:lch-partition-of-unity}, there exists a partition of unity $\seqf{\phi_j} \subset C_c(X; [0, 1])$ on $\supp{\phi}$ subordinate to $\seqf{V_j}$. For any $x \in E$, 
     \begin{align*}
         \phi(x) - \sum_{j = 1}^n y_j \phi_j(x) &= \sum_{j = 1}^n \phi(x) \phi_j(x) - \sum_{j = 1}^n y_j \phi_j(x) \\
         &= \sum_{j = 1}^n \phi_j(x)[\phi(x) - y_j] \in \sum_{j = 1}^n \phi_j(x)U \subset U

src/topology/main/compactify.tex

@@ -104,7 +104,7 @@
         \item $\infty \in U$ and $U^c \subset X$ is compact. 
     \end{enumerate}
 
-    Let $\seqi{U} \subset \mathcal{T}^*$ be an open cover of $X$, then there exists $i \in I$ such that $\infty \in U$. In which case, $U_i$ must satisfy (b), so there exists $J \subset I$ finite such that $\bigcup_{j \in J}U_j \supset U_i^c$, and $\bracsn{U_j|j \in J \cup \bracs{i}}$ is a finite subcover. Now, let $x \in X$, then since $X$ is locally compact, there exists a precompact neighbourhood $U \in \cn_X^o(x)$. In which case, $\ol{U}^c \in  \cn_{X^*}(\infty)$ with $U \cap \ol{U}^c = \emptyset$. Therefore $X^*$ is a compact Hausdorff space. 
+    Let $\seqi{U} \subset \mathcal{T}^*$ be an open cover of $X$, then there exists $i \in I$ such that $\infty \in U$. In which case, $U_i$ must satisfy (b), so there exists $J \subset I$ finite such that $\bigcup_{j \in J}U_j \supset U_i^c$, and $\bracsn{U_j|j \in J \cup \bracs{i}}$ is a finite subcover. Now, let $x \in X$, then since $X$ is locally compact, there exists a relatively compact neighbourhood $U \in \cn_X^o(x)$. In which case, $\ol{U}^c \in  \cn_{X^*}(\infty)$ with $U \cap \ol{U}^c = \emptyset$. Therefore $X^*$ is a compact Hausdorff space. 
     
     Let $\iota: X \to X^*$ be the inclusion map. For each $U \in \mathcal{T}^*$ satisfying (b), $\iota^{-1}(U) = U \cap X$. Since $U^c \subset X$ is compact, $U \cap X$ is open by \autoref{proposition:compact-closed}, so $\iota \in C(X; X^*)$. By (a), $\iota$ is an embedding. 
 

src/topology/main/definition.tex

@@ -164,7 +164,7 @@
 \label{definition:ideal-generated-topology}
     Let $X$ be a topological space and $\sigma \subset 2^X$ be an ideal, then $X$ is \textbf{$\sigma$-generated} if the topology of $X$ is the final topology generated by $\bracs{\iota_S: S \to X|S \in \sigma}$. 
 
-    If $\kappa \subset 2^X$ is the collection of precompact sets of $X$, and $X$ is generated by $\kappa$, then $X$ is \textbf{compactly generated}. 
+    If $\kappa \subset 2^X$ is the collection of relatively compact sets of $X$, and $X$ is generated by $\kappa$, then $X$ is \textbf{compactly generated}. 
 \end{definition}
 
 

src/topology/main/lch.tex

@@ -7,7 +7,7 @@
     \begin{enumerate}
         \item For any $x \in X$, there exists $K \in \cn(x)$ compact.
         \item For any $x \in X$, $\cn(x)$ admits a fundamental system of neighbourhoods consisting of compact sets.
-        \item For any $x \in X$, $\cn(x)$ admits a fundamental system of neighbourhoods consisting of precompact sets.
+        \item For any $x \in X$, $\cn(x)$ admits a fundamental system of neighbourhoods consisting of relatively compact sets.
     \end{enumerate}
 
     If the above holds, then $X$ is a \textbf{locally compact Hausdorff (LCH)} space.
@@ -20,10 +20,10 @@
 
 \begin{lemma}
 \label{lemma:lch-compact-neighbour}
-    Let $X$ be a LCH space, $K \subset X$ be compact, and $U \in \cn(K)$, then there exits $V \in \cn^o(K)$ precompact such that $K \subset V \subset \ol{V} \subset U$.
+    Let $X$ be a LCH space, $K \subset X$ be compact, and $U \in \cn(K)$, then there exits $V \in \cn^o(K)$ relatively compact such that $K \subset V \subset \ol{V} \subset U$.
 \end{lemma}
 \begin{proof}
-    For each $x \in K$, there exists $V_x \in \cn^o(x)$ be precompact such that $x \in V_x \subset \overline{V_x} \subset U$ by (3) of \autoref{definition:lch}. Since $K$ is compact, there exists $\seqf{x_j} \subset K$ such that
+    For each $x \in K$, there exists $V_x \in \cn^o(x)$ be relatively compact such that $x \in V_x \subset \overline{V_x} \subset U$ by (3) of \autoref{definition:lch}. Since $K$ is compact, there exists $\seqf{x_j} \subset K$ such that
     \[
     K \subset \bigcup_{j = 1}^n V_{x_j} \subset U
     \]
@@ -33,7 +33,7 @@
     \ol{\bigcup_{j = 1}^n V_{x_j}} = \bigcup_{j = 1}^n \overline{V_{x_j}} \subset U
     \]
 
-    so $V = \bigcup_{j = 1}^n V_{x_j} \in \cn^o(K)$ is precompact.
+    so $V = \bigcup_{j = 1}^n V_{x_j} \in \cn^o(K)$ is relatively compact.
 \end{proof}
 
 \begin{lemma}[Urysohn's Lemma (LCH)]
@@ -41,7 +41,7 @@
     Let $X$ be a LCH space, $K \subset X$ be compact, and $U \in \cn(K)$, then there exists $F \in C_c(X; [0, 1])$ such that $\supp{F} \subset U$.
 \end{lemma}
 \begin{proof}[Proof, {{\cite[Lemma 4.32]{Folland}}}. ]
-    By \autoref{lemma:lch-compact-neighbour}, there exists $V, W \in \cn^o(K)$ precompact such that
+    By \autoref{lemma:lch-compact-neighbour}, there exists $V, W \in \cn^o(K)$ relatively compact such that
     \[
     K \subset V \subset \ol{V} \subset W \subset \ol{W} \subset U
     \]
@@ -64,7 +64,7 @@
     Let $X$ be a LCH space, $K \subset X$ be compact, $U \in \cn^o(K)$, and $f \in C(K; \real)$, then there exists $F \in C_c(U; \real)$ such that $F|_K = f$.
 \end{theorem}
 \begin{proof}
-    By \autoref{lemma:lch-compact-neighbour}, there exists $V, W \in \cn^o(K)$ precompact such that $K \subset V \subset \ol{V} \subset U$. As $\ol{W}$ is compact, it is normal by \autoref{proposition:compact-hausdorff-normal}. Since $X$ is Hausdorff, $K \subset \ol{W}$ is closed by \autoref{proposition:compact-closed}.
+    By \autoref{lemma:lch-compact-neighbour}, there exists $V, W \in \cn^o(K)$ relatively compact such that $K \subset V \subset \ol{V} \subset U$. As $\ol{W}$ is compact, it is normal by \autoref{proposition:compact-hausdorff-normal}. Since $X$ is Hausdorff, $K \subset \ol{W}$ is closed by \autoref{proposition:compact-closed}.
 
     By the \hyperref[Tietze extension theorem]{theorem:tietze}, there exists $F \in C(\ol{W}; \real)$ such that $F|_K = f$. By \hyperref[Urysohn's lemma]{lemma:lch-urysohn}, there exists $\eta \in C_c(X; [0, 1])$ such that $\eta|_K = 1$ and $\supp{\eta} \subset V$. In which case, define
     \[
@@ -119,12 +119,12 @@
 
     Assume inductively that $\bracs{U_j}_0^n$ has been constructed such that:
     \begin{enumerate}
-        \item[(a)] For each $0 \le k \le n$, $U_k$ is a precompact open set.
+        \item[(a)] For each $0 \le k \le n$, $U_k$ is a relatively compact open set.
         \item[(b)] For each $0 \le k < n$, $\overline{U_k} \subset U_{k+1}$.
         \item[(c)] For each $1 \le k \le n$, $U_k \supset \bigcup_{j = 1}^k K_j$.
     \end{enumerate}
 
-    By \autoref{lemma:lch-compact-neighbour}, there exists $U_{n+1} \in \cn^o(\overline{U_n} \cup K_{n+1})$ precompact. In which case, by (c),
+    By \autoref{lemma:lch-compact-neighbour}, there exists $U_{n+1} \in \cn^o(\overline{U_n} \cup K_{n+1})$ relatively compact. In which case, by (c),
     \[
     U_{n+1} \supset \ol{U_n} \cup K_{n+1} \supset \bigcup_{j = 1}^n K_j \cup K_{n+1} = \bigcup_{j = 1}^{n+1}K_j
     \]
@@ -159,8 +159,8 @@
 \end{proof}
 
 \begin{lemma}
-\label{lemma:lch-locally-finite-precompact-refine}
+\label{lemma:lch-locally-finite-relatively compact-refine}
-    Let $X$ be a LCH space and $\ce \subset 2^X$ be a locally finite precompact open cover of $X$, then there exists locally finite precompact open covers $\bracs{F_E}_{E \in \ce}, \bracs{G_E}_{E \in \ce} \subset 2^X$ such that for each $E \in \ce$, $F_E \subset \ol{F_E} \subset E \subset \ol{E} \subset G_E$.
+    Let $X$ be a LCH space and $\ce \subset 2^X$ be a locally finite relatively compact open cover of $X$, then there exists locally finite relatively compact open covers $\bracs{F_E}_{E \in \ce}, \bracs{G_E}_{E \in \ce} \subset 2^X$ such that for each $E \in \ce$, $F_E \subset \ol{F_E} \subset E \subset \ol{E} \subset G_E$.
 \end{lemma}
 \begin{proof}
     $(\bracs{F_E}_{E \in \ce})$: For each $E \in \ce$, $\bracs{F \in \ce|F \cap \ol E \ne \emptyset}$ is finite by \autoref{lemma:locally-finite-compact}. Let
@@ -168,7 +168,7 @@
     F_E = \bigcup_{\substack{F \in \ce} \\ F \cap \ol E \ne \emptyset}F
     \]
 
-    then $F_E \in \cn(\ol{E})$ is precompact.
+    then $F_E \in \cn(\ol{E})$ is relatively compact.
 
     Let $N \subset X$ and $E \in \ce$. If $N \cap F_E \ne \emptyset$, then there exists $F \in \ce$ such that $N \cap F \ne \emptyset$ and $F \cap \ol{E} \ne \emptyset$. Thus
     \[
@@ -179,7 +179,7 @@
 
     Let $x \in X$, then there exists $N \in \cn(x)$ such that $\bracs{F \in \ce|N \cap F \ne \emptyset}$ is finite. In which case, $\bracs{E \in \ce|N \cap F_E \ne \emptyset}$ is finite as well. Therefore $\bracs{F_E}_{E \in \ce}$ is locally finite.
 
-    $(\bracs{G_E}_{E \in \ce})$: For each $x \in X$, there exists $E \in \ce$ and $N_x \in \cn^o(x)$ precompact with $x \in N_x \subset \ol{N_x} \subset E$.
+    $(\bracs{G_E}_{E \in \ce})$: For each $x \in X$, there exists $E \in \ce$ and $N_x \in \cn^o(x)$ relatively compact with $x \in N_x \subset \ol{N_x} \subset E$.
 
     For any $E \in \ce$, $\ol{E}$ is compact, so there exists $X_E \subset X$ finite such that
     \begin{enumerate}
@@ -212,35 +212,35 @@
     Let $X$ be a LCH space, then the following are equivalent:
     \begin{enumerate}
         \item $X$ is paracompact.
-        \item There exists a locally finite precompact open cover $\cf$ of $X$.
+        \item There exists a locally finite relatively compact open cover $\cf$ of $X$.
-        \item For any open cover $\mathcal{U}$ of $X$, there exists a locally finite refinement $\mathcal{V}$ of $\mathcal{U}$ consisting of precompact open sets.
+        \item For any open cover $\mathcal{U}$ of $X$, there exists a locally finite refinement $\mathcal{V}$ of $\mathcal{U}$ consisting of relatively compact open sets.
-        \item For any open cover $\mathcal{U}$ of $X$, there exists locally finite refinements $\seqi{V}, \seqi{W} \subset 2^X$ of $\mathcal{U}$ consisting of precompact open sets such that $\ol{W_i} \subset V_i$ for all $i \in I$.
+        \item For any open cover $\mathcal{U}$ of $X$, there exists locally finite refinements $\seqi{V}, \seqi{W} \subset 2^X$ of $\mathcal{U}$ consisting of relatively compact open sets such that $\ol{W_i} \subset V_i$ for all $i \in I$.
         \item For any open cover $\mathcal{U}$ of $X$, there exists a $C_c(X; [0, 1])$ partition of unity subordinate to it.
         \item $X$ admits a $C_c(X; [0, 1])$ partition of unity.
     \end{enumerate}
 \end{proposition}
 \begin{proof}
-    (1) $\Rightarrow$ (2): For each $x \in X$, there exists a precompact open neighbourhood $U_x \in \cn^o(x)$. Since $\bracs{U_x| x \in X}$ is an open cover of $X$, there exists a locally finite refinement $\mathcal{V}$. For each $V \in \mathcal{V}$, there exists $x \in X$ such that $V \subset U_x$. In which case, $\ol{V} \subset \ol{U_x}$ is compact.
+    (1) $\Rightarrow$ (2): For each $x \in X$, there exists a relatively compact open neighbourhood $U_x \in \cn^o(x)$. Since $\bracs{U_x| x \in X}$ is an open cover of $X$, there exists a locally finite refinement $\mathcal{V}$. For each $V \in \mathcal{V}$, there exists $x \in X$ such that $V \subset U_x$. In which case, $\ol{V} \subset \ol{U_x}$ is compact.
 
-    (2) $\Rightarrow$ (3): Let $\cf \subset 2^X$ be a locally finite open cover of $X$ consisting of precompact open sets. By \autoref{lemma:lch-locally-finite-precompact-refine}, there exists a locally finite open cover $\bracs{G_F}_{F \in \cf}$ of $X$ consisting of precompact open sets such that $\ol{F} \subset G_F$ for all $F \in \cf$.
+    (2) $\Rightarrow$ (3): Let $\cf \subset 2^X$ be a locally finite open cover of $X$ consisting of relatively compact open sets. By \autoref{lemma:lch-locally-finite-relatively compact-refine}, there exists a locally finite open cover $\bracs{G_F}_{F \in \cf}$ of $X$ consisting of relatively compact open sets such that $\ol{F} \subset G_F$ for all $F \in \cf$.
 
     For each $F \in \cf$, let
     \[
     \mathcal{U}_F = \bracs{U \cap G_F|U \in \mathcal{U}}
     \]
 
-    then $\mathcal{U}_F$ is a precompact open cover of $\ol{F}$. By compactness of $\ol{F}$, there exists $\mathcal{V}_F \subset \mathcal{U}_F$ finite such that $\ol{F} \subset \bigcup_{V \in \mathcal{V}_F}V$.
+    then $\mathcal{U}_F$ is a relatively compact open cover of $\ol{F}$. By compactness of $\ol{F}$, there exists $\mathcal{V}_F \subset \mathcal{U}_F$ finite such that $\ol{F} \subset \bigcup_{V \in \mathcal{V}_F}V$.
 
-    Let $\mathcal{V} = \bigcup_{F \in \cf}\mathcal{V}_F$, then $\mathcal{V}$ is a precompact open cover of $X$. For any $x \in X$, there exists $N \in \cn(x)$ such that $\bracs{F \in \cf|N \cap G_F}$ is finite. Thus
+    Let $\mathcal{V} = \bigcup_{F \in \cf}\mathcal{V}_F$, then $\mathcal{V}$ is a relatively compact open cover of $X$. For any $x \in X$, there exists $N \in \cn(x)$ such that $\bracs{F \in \cf|N \cap G_F}$ is finite. Thus
     \[
     \bracs{V \in \mathcal{V}| N \cap V} \subset \bigcup_{\substack{F \in \cf \\ N \cap G_F \ne \emptyset}}\mathcal{V}_F
     \]
 
     is finite, and $\mathcal{V}$ is locally finite.
 
-    (3) $\Rightarrow$ (4): By \autoref{lemma:lch-locally-finite-precompact-refine}.
+    (3) $\Rightarrow$ (4): By \autoref{lemma:lch-locally-finite-relatively compact-refine}.
 
-    (4) $\Rightarrow$ (5): Let $\seqi{V}, \seqi{W} \subset 2^X$ be locally finite refinements of $\mathcal{U}$ consisting of precompact open sets such that for each $i \in I$, $\ol{W_i} \subset V_i$.
+    (4) $\Rightarrow$ (5): Let $\seqi{V}, \seqi{W} \subset 2^X$ be locally finite refinements of $\mathcal{U}$ consisting of relatively compact open sets such that for each $i \in I$, $\ol{W_i} \subset V_i$.
 
     By \hyperref[Urysohn's lemma]{lemma:lch-urysohn}, there exists $\seqi{f} \in C_c(X; [0, 1])$ such that for each $i \in I$, $f_i|_{\ol{W_i}} = 1$ and $\supp{f_i} \subset V_i$.
 
@@ -257,7 +257,7 @@
 
     (5) $\Rightarrow$ (6): Take $\mathcal{U} = \bracs{X}$.
 
-    (6) $\Rightarrow$ (2): Let $\seqi{f} \subset C_c(X; [0, 1])$ be a partition of unity. For each $i \in I$, let $V_i = \bracs{f_i > 0}$, then $\seqi{V}$ is a locally finite precompact open cover of $\mathcal{U}$.
+    (6) $\Rightarrow$ (2): Let $\seqi{f} \subset C_c(X; [0, 1])$ be a partition of unity. For each $i \in I$, let $V_i = \bracs{f_i > 0}$, then $\seqi{V}$ is a locally finite relatively compact open cover of $\mathcal{U}$.
 \end{proof}
 
 \begin{proposition}
@@ -273,7 +273,7 @@
     Let $X$ be a $\sigma$-compact LCH space, then $X$ is paracompact.
 \end{proposition}
 \begin{proof}
-    By \autoref{proposition:lch-sigma-compact}, there exists an exhaustion $\seq{U_n} \subset 2^X$ of $X$ by precompact open sets. Denote $U_0 = \emptyset$. For each $n \in \natp$, let $V_n = U_{n+1} \setminus \ol{U_{n-1}}$.
+    By \autoref{proposition:lch-sigma-compact}, there exists an exhaustion $\seq{U_n} \subset 2^X$ of $X$ by relatively compact open sets. Denote $U_0 = \emptyset$. For each $n \in \natp$, let $V_n = U_{n+1} \setminus \ol{U_{n-1}}$.
 
     Let $x \in X$, then there exists $n \in \natp$ such that $x \in U_n \setminus U_{n-1}$. In which case, if $n > 1$, then $x \in U_{n} \setminus \ol{U_{n - 2}} = V_{n-1}$. If $n = 1$, then $x \in U_{2} = V_1$. Thus $\seq{V_n}$ is an open cover of $X$. In addition, for any $m, n \in \natp$ with $m \le n$, $V_m \cap V_n \ne \emptyset$ implies that $n - m < 2$, so $\seq{V_n}$ is locally finite. By (2) of \autoref{proposition:lch-paracompact}, $X$ is paracompact.
 \end{proof}

src/topology/uniform/equicontinuous.tex

@@ -49,12 +49,12 @@
 
     In addition, if $\cf$ satisfies (E1) and
     \begin{enumerate}[label=(E\arabic*), start=1]
-        \item For each $x \in X$, $\cf(x) = \bracs{f(x)|f \in \cf}$ is precompact in $Y$.
+        \item For each $x \in X$, $\cf(x) = \bracs{f(x)|f \in \cf}$ is relatively compact in $Y$.
     \end{enumerate}
 
     then
     \begin{enumerate}[label=(C\arabic*), start=2]
-        \item $\cf$ is a precompact subset of $C(X; Y)$ with respect to the uniform structure of compact convergence. 
+        \item $\cf$ is a relatively compact subset of $C(X; Y)$ with respect to the uniform structure of compact convergence. 
     \end{enumerate}
 
     Conversely, if $X$ is a LCH space, then (C3) implies (E1) + (E2).