Added the fundamental theorem of calculus.

src/fa/rs/bv.tex

@@ -6,7 +6,7 @@
 \label{definition:total-variation}
     Let $E$ be a locally convex space, $\rho$ be a continuous seminorm on $E$, $f: [a, b] \to E$, and $P \in \scp([a, b])$ be a partition, then
     \[
-    V_{\rho, p}(f) = \sum_{j = 1}^n \rho(f(x_j) - f(x_{j - 1}))
+    V_{\rho, P}(f) = \sum_{j = 1}^n \rho(f(x_j) - f(x_{j - 1}))
     \]
 
     is the \textbf{variation} of $f$ with respect to $\rho$ and $P$. The supremum over all such partitions
@@ -19,7 +19,45 @@
     If $E$ is a normed vector space, then the variation and total variation of $f$ is taken with respect to its norm.
 \end{definition}
 
-\begin{definition}[Bounded Variation, {{\cite[Proposition X.1.1]{Lang}}}]
+\begin{definition}[Variation Function]
+\label{definition:variation-function}
+    Let $E$ be a locally convex space, $\rho$ be a continuous seminorm on $E$, $f: [a, b] \to E$, then the function
+    \[
+    T_{f, \rho}(x) = \sup_{P \in \scp([a, x])}V_{\rho, P}(f) = [f|_{[a, x]}]_{\text{var}, \rho}
+    \]
+
+    is the \textbf{variation function} of $f$ with respect to $\rho$, and:
+    \begin{enumerate}
+        \item $T_{f, \rho}: [a, b] \to [0, \infty]$ is a non-negative, non-decreasing function. 
+        \item If $f \in BV([a, b]; E)$, then for any $[c, d] \subset [a, b]$, $[f]_{\text{var}, \rho} = T_{f, \rho}(d) - T_{f, \rho}(a)$. 
+    \end{enumerate}
+\end{definition}
+\begin{proof}
+    (2): Let $P \in \scp([a, c])$ and $Q = \seqf{x_j} \in \scp([a, d])$ be partitions containing $P$, then
+    \[
+    V_{\rho, Q}(f) - V_{\rho, P}(f) = \sum_{x_j > c}\rho(f(x_j) - f(x_{j - 1})) \le [f]_{\text{var}, \rho}
+    \]
+
+    As this holds for all $Q \in \scp([a, d])$ containing $P$, 
+    \[
+    T_{f, \rho}(d) - T_{f, \rho}(c) \le T_{f, \rho}(d) - V_{\rho, P}(f) \le [f|_{[c, d]}]_{\text{var}, \rho}
+    \]
+
+    On the other hand, for any $R \in \scp([c, d])$, $P \cup R \in \scp([a, d])$ and contains $P$. Therefore
+    \[
+    T_{f, \rho}(d) - V_{\rho, P}(f) \ge V_{\rho, R \cup P}(f) - V_{\rho, P}(f) = V_{\rho, R}(f)
+    \]
+
+    Since this holds for all $P \in \scp([a, c])$, 
+    \[
+    T_{f, \rho}(d) - T_{f, \rho}(c) \ge V_{\rho, R}(f)
+    \]
+
+    and as the above holds for all $R \in \scp([c, d])$, $T_{f, \rho}(d) - T_{f, \rho}(c) \ge [f|_{[c, d]}]_{\text{var}, \rho}$. 
+\end{proof}
+
+
+\begin{definition}[Bounded Variation]
 \label{definition:bounded-variation}
     Let $E$ be a locally convex space, $\rho$ be a continuous seminorm on $E$, and $f: [a, b] \to E$. If $[f]_{\text{var}, \rho} < \infty$, then $f$ is of \textbf{bounded variation} with respect to $\rho$.
 
@@ -40,7 +78,7 @@
         \item[(5)] $f$ has at most countably many discontinuities.
     \end{enumerate}
 \end{definition}
-\begin{proof}
+\begin{proof}[Proof {{\cite[Proposition X.1.1]{Lang}}}. ]
     (3): Let $\rho$ be a continuous seminorm on $E$ and $P \in \scp([a, b])$, then by assumption (a),
     \[
     V_{\rho, P}(f) = \sum_{j = 1}^n \rho(f(x_j) - f(x_{j - 1}))
@@ -71,7 +109,19 @@
 
 \begin{proposition}
 \label{proposition:bounded-variation-one-side-limit}
-    
+    Let $E$ be a complete locally convex space and $f \in BV([a, b]; E)$, then for each $x \in [a, b]$, the limits $\lim_{y \downto x}f(y)$ and $\lim_{y \upto x}f(y)$ exist. 
 \end{proposition}
+\begin{proof}
+    By flipping $f$, it is sufficient to consider the right-side limit $\lim_{y \downto x}f(y)$. 
+    
+    Let $\rho: E \to [0, \infty)$ be a continuous seminorm on $E$, and $T_{\rho, f}: [a, b] \to [0, \infty)$ be the variation function of $f$ with respect to $\rho$. For any $\eps > 0$, there exists $\delta > 0$ such that $T_{\rho, f}(z) - \lim_{y \downto x}T_{\rho, f}(y) < \eps$ for all $z \in (x, x + \delta)$. In which case, for any $x < y < z < x + \delta$, 
+    \[
+    \rho(f(z) - f(y)) \le [f|_{y, z}]_{\text{var}, \rho} \le T_{\rho, f}(z) - T_{\rho, f}(y) \le T_{\rho, f}(z) - \lim_{u \downto x}T_{\rho, f}(u) < \eps
+    \]
+
+    By completeness of $E$, the limit $\lim_{y \downto x}f(y)$ exists. 
+\end{proof}
+
+
 
 

src/fa/rs/index.tex

@@ -5,3 +5,5 @@
 \input{./bv.tex}
 \input{./rs.tex}
 \input{./rs-bv.tex}
+\input{./regulated.tex}
+\input{./rs-measure.tex}

src/fa/rs/regulated.tex

@@ -0,0 +1,109 @@
+\section{Regulated Functions}
+\label{section:regulated-function}
+
+
+\begin{proposition}
+\label{proposition:rs-interval}
+    Let $[a, b] \subset \real$, $E, F, H$ be TVSs over $K \in \RC$, and $E \times F \to H$ with $(x, y) \mapsto xy$ be a continuous linear map. 
+    
+    Let $G: [a, b] \to F$ and $[c, d] \subset [a, b]$ such that $G$ is continuous at $c$ and $d$, then for any $x \in E$, $x \cdot \one_{[c, d]} \in RS([a, b], G)$, and
+    \[
+    \int_a^b x \cdot \one_{[c, d]} dG = x \cdot [G(d) - G(c)]
+    \]
+\end{proposition}
+\begin{proof}
+    Assume without loss of generality that $a < c \le d < b$. Let $U \in \cn_H(0)$, then there exists $V \in \cn_F(0)$ such that $xV \subset U$. By continuity of $G$, there exists $\delta > 0$ such that $G((c - \delta, c]) - G(c) \subset V$ and $G([d, d + \delta)) - G(d) \subset V$. In which case, for any tagged partition $(P = \bracsn{x_j}_0^n, t = \seqf{t_j})$ that contains $\bracs{c - \delta, c, d, d + \delta}$, 
+    \begin{align*}
+        S(Q, t, x \cdot \one_{[c, d]}, G) &= x\sum_{a < x_j \le c - \delta}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\
+        &+ x \sum_{c - \delta < x_j \le c}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\
+        &+ x \sum_{c < x_j \le d}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j-1})] \\
+        &+ x \sum_{d < x_j \le d + \delta}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\
+        &+ x \sum_{d + \delta < x_j \le b}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\
+        &= x \sum_{c - \delta \le x_j \le c}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\
+        &+ x \cdot [G(d) - G(c)] \\
+        &+ x \sum_{d < x_j \le d + \delta}\one_{[c, d]}[G(x_j) - G(x_{j - 1})] \\
+        &\in G(d) - G(c) + xG([c - \delta, c]) + xG([d, d + \delta]) \\
+        &\subset x \cdot [G(d) - G(c)] + xV + xV \subset [G(d) - G(c)] + U + U
+    \end{align*}
+\end{proof}
+
+
+\begin{definition}[Step Map]
+\label{definition:step-map}
+    Let $[a, b] \subset \real$, $E$ be a TVS, $f: [a, b] \to E$ be a function, and $P = \bracsn{x_j}_1^n \in \scp([a, b])$, then $f$ is a \textbf{step map} with respect to $P$ if for each $1 \le j \le n$, $f$ is constant on $(x_{j - 1}, x_j)$. 
+\end{definition}
+
+\begin{definition}[Regulated Function]
+\label{definition:regulated-function}
+    Let $[a, b] \subset \real$, $E, F, H$ be TVSs over $K \in \RC$, and $E \times F \to H$ with $(x, y) \mapsto xy$ be a continuous linear map. 
+
+    Let $G: [a, b] \to F$ and $f: [a, b] \to E$ be a step map, then $f$ is \textbf{regulated with respect to} $G$ if $f$ is continuous on all discontinuity points of $G$. Let $\text{Reg}([a, b], G; E)$ be closure of all regulated step maps with respect to the uniform norm, then:
+    \begin{enumerate}
+        \item Every regulated step map is in $RS([a, b], G)$. 
+        \item If $E$ is metrisable, then for any $f \in \text{Reg}([a, b], G; E)$, $f$ is continuous at all but at most countably many points, and $f$ does not share any discontinuity points with $E$. 
+        \item If $E, F, H$ are locally convex, $G \in BV([a, b]; F)$, and $H$ is complete, then $\text{Reg}([a, b], G; E) \subset RS([a, b], G)$. 
+        \item If $F$ is normed and $G \in BV([a, b]; F)$, then $\text{Reg}([a, b], G; E) \supset C([a, b]; E)$.
+    \end{enumerate}
+
+    The set $\text{Reg}([a, b], G; E)$ is the space of \textbf{regulated functions} with respect to $G$. If $G = \text{Id}$, then $\text{Reg}([a, b]; E) = \text{Reg}([a, b], G; E)$ denotes the space of regulated functions on $[a, b]$.
+\end{definition}
+\begin{proof}
+    (1): If $f: [a, b] \to E$ is a regulated step map, then there exists $\seqf{[a_j, b_j]} \subset 2^{[a, b]}$ and $\seqf{x_j}$ such that
+    \begin{enumerate}
+        \item $f = \sum_{j = 1}^n x_j \one_{[a_j, b_j]}$.
+        \item For each $1 \le j \le n$, $G$ is continuous at $a_j$ and $b_j$. 
+    \end{enumerate}
+
+    Thus $f \in RS([a, b], G)$ by \autoref{proposition:rs-interval}. 
+
+    (2): Let $f \in \text{Reg}([a, b], G; E)$, then there exists regulated step maps $\seq{f_n} \subset \text{Reg}([a, b], G; E)$ such that $f_n \to f$ uniformly. For each $n \in \natp$, let $D_n$ be the set of discontinuity points of $f_n$. Let $x \in [a, b] \setminus \bigcup_{n \in \natp}D_n$. For any symmetric neighbourhood $U \in \cn_E(0)$, there exists $n \in \natp$ such that $(f_n - f)([a, b]) \subset U$. Since $f_n$ is continuous at $x$, there exists $\eps > 0$ such that $f_n((x - \eps, x + \eps)) - f_n(x) \in U$. In which case,
+    \begin{align*}
+        f((x - \eps, x + \eps)) - f(x) &\subset (f_n - f)((x - \eps, x + \eps)) + (f_n - f)(x) \\
+        &+ f_n((x - \eps, x + \eps)) - f_n(x) \\
+        &\subset U + U + U 
+    \end{align*}
+
+    Therefore $f$ is continuous at $x$. Since each $D_n$ is finite, $\bigcup_{n \in \natp}D_n$ is countable. Given that $G$ is continuous on every point in each $D_n$, $G$ is also continuous on all the discontinuity points of $f$. 
+
+    (3): Suppose that $E, F, H$ are locally convex, $G \in BV([a, b]; F)$, and $H$ is complete. Let $f \in \text{Reg}([a, b], G; E)$, then there exists regulated step maps $\net{f} \subset \text{Reg}([a, b], G; E)$ such that $f_\alpha \to f$ uniformly. By \autoref{proposition:rs-complete}, $f \in RS([a, b], G)$. Therefore $\text{Reg}([a, b], G; E) \subset RS([a, b], G)$. 
+    
+    (4): If $F$ is normed and $G \in BV([a, b]; F)$, then $G$ has at most countably many discontinuities by \autoref{definition:bounded-variation}, so the continuity points of $G$ are dense in $[a, b]$. 
+
+    Let $f \in C([a, b]; E)$, then $f \in UC([a, b]; E)$ by \autoref{proposition:uniform-continuous-compact}. Let $U \in \cn_E(0)$, then there exists a partition $P = \bracsn{x_j}_1^n \in \scp([a, b])$ such that for each $1 \le j \le n$ and $x, y \in [x_{j-1}, x_j]$, $f(x) - f(y) \in U$. In which case, let
+    \[
+    \phi = f(a)\one_{\bracs{a}} + \sum_{j = 1}^n f(x_j)\one_{(x_{j - 1}, x_j]}
+    \]
+
+    then $\phi$ is a regulated step map with $(\phi - f)([a, b]) \in U$. 
+\end{proof}
+
+\begin{theorem}[Fundamental Theorem of Calculus for Riemann Integrals]
+\label{theorem:ftc-riemann}
+    Let $[a, b] \subset \real$ and $E$ be a separated locally convex space, then:
+    \begin{enumerate}
+        \item For any Riemann integrable function $f: [a, b] \to E$ and $x \in (a, b)$ such that $f$ is continuous at $x$, the function
+        \[
+        F: [a, b] \to E \quad y \mapsto \int_a^y f(t)dt
+        \]
+
+        is differentiable at $x$ with $DF(x) = f(x)$. 
+
+        \item For $F \in C^1([a, b]; E)$, 
+        \[
+        F(b) - F(a) = \int_a^b DF(t)dt
+        \]
+    \end{enumerate}
+\end{theorem}
+\begin{proof}
+    (1): Let $x_0 \in (a, b)$ such that $f$ is continuous at $x$, and $\delta > 0$ such that $(x_0 - \delta, x_0 + \delta) \subset (a, b)$, then for any $h > 0$, 
+    \begin{align*}
+        \frac{1}{h}\braks{\int_a^{x+h} f(t)dt - \int_a^{x} f(t)dt} &= \frac{1}{h}\int_x^{x+h}f(t)dt \in \overline{\text{Conv}(f([t, t +h)))} \\
+        -\frac{1}{h}\braks{\int_a^{x-h} f(t)dt - \int_a^{x} f(t)dt} &= \frac{1}{h}\int_{x-h}^{x}f(t)dt \in \overline{\text{Conv}(f([t, t +h)))}
+    \end{align*}
+
+    As $E$ is locally convex and separated, and $f$ is continuous at $x$, this implies that $[F(x + h) - F(x)]/h \to f(x)$.  
+
+    (2): Let $G(x) = \int_a^x DF(t)dt + F(a)$, then $G - F$ has derivative $0$. By the \hyperref[Mean Value Theorem]{proposition:zero-derivative-constant}, $G - F$ is constant. As $G(a) - F(a) = 0$, $G  = F$. 
+    
+\end{proof}
+

src/fa/rs/rs-measure.tex

@@ -1,23 +1,92 @@
 \section{The Lebesgue-Stieltjes Integral}
 \label{section:riemann-lebesgue-stieltjes}
 
-\begin{theorem}
+\begin{definition}[Lebesgue-Stieltjes Measure]
-\label{theorem:riemann-lebesgue-stieltjes}
+\label{definition:riemann-lebesgue-stieltjes}
     Let $[a, b] \subset \real$, $E$ be a Banach space, and $G \in BV([a, b]; E^*)$, then there exists a unique $\mu_G \in M_R([a, b]; E^*)$ such that:
     \begin{enumerate}
-        \item For any $f \in C([a, b]; E)$, 
+        \item For any $f \in \text{Reg}([a, b], G; E)$, 
         \[
-        \int f(t) G(dt) = \int \dpn{f(t), \mu_G(dt)}{E}
+        \int_a^b f(t) G(dt) = \int_{[a, b]} \dpn{f(t), \mu_G(dt)}{E}
         \]
 
-        \item For any 
+        \item For any $a \le c < d < b$, 
-
+        \[
-        \item For any $a \le c < d \le b$ such that $G$ is continuous on $c$ and $d$, $\mu_G((c, d]) = G(d) - G(c)$.
+        \mu_G((c, d]) = G(d+) - G(c+) = \lim_{z \downto d}G(z) - \lim_{z \downto c}G(z)
+        \]
     \end{enumerate}
-\end{theorem}
-\begin{proof}
-    (1): By \autoref{proposition:rs-bv-continuous}, the mapping $f \mapsto \int f(t)G(dt)$ is a continuous linear functional on $C_0([a, b]; E) = C([a, b]; E)$. Thus (1) holds by \hyperref[Singer's Representation Theorem]{theorem:singer-representation}.
 
-    (2): 
+    The measure $\mu_G$ is the \textbf{Lebesgue-Stieltjes measure} associated with $G$.
+\end{definition}
+\begin{proof}
+    By \autoref{proposition:rs-bv-continuous}, the mapping $f \mapsto \int f(t)G(dt)$ is a continuous linear functional on $C_0([a, b]; E) = C([a, b]; E)$. By \hyperref[Singer's Representation Theorem]{theorem:singer-representation}, there exists $\mu_G \in M_R([a, b]; E^*)$ such that (1) holds for $C([a, b], G; E)$.
+
+    (2): Fix $x \in [a, b)$. For each $u \in (x, b)$, there exists a non-increasing function $\phi_u \in C_c([a, b))$ such that $\phi_u|_{[a, x]} = 1$ and $\supp{\phi_u} \subset [a, u]$. By outer regularity of $\mu_G$, 
+    \[
+    \mu_G([a, x]) = \lim_{u \downto x}\mu_G([a, u]) = \lim_{u \downto x}\int_{[a, b]}\phi_u d\mu_G = \lim_{u \downto x}\int_a^b \phi_u dG
+    \]
+
+    For each $u > x$, using \hyperref[integration by parts]{theorem:rs-ibp}, 
+    \begin{align*}
+        \int_a^b \phi_u dG &= \phi(b)G(b) - \phi(a)G(a) - \int_a^b G d\phi_u \\
+        &= - G(a) - \int_a^b G d\phi_u
+    \end{align*}
+
+    Let $v \in (x, u)$ and $(P = \bracs{x_j}_0^n, c = \bracs{c_j}_1^n)$ be a tagged partition containing $\bracs{x, v, u}$, then since $\phi_u$ is non-increasing, 
+    \begin{align*}
+        \int_a^b Gd\phi_u &= \sum_{x < x_j \le v}G(c_j)[\phi(x_j) - \phi(x_{j - 1})] + \sum_{v < x_j \le u}G(c_j)[\phi(x_j) - \phi(x_{j - 1})] \\
+        &\in [\phi(v) - \phi(x)]G([x, u]) + [\phi(u) - \phi(v)]G((x, u]) \\
+        &\subset [\phi(v) - \phi(x)]G([x, u]) - G((x, u])
+    \end{align*}
+    
+
+    Since the above holds for all $v \in (x, u)$, $\int_a^b Gd\phi_u \in -\overline{G((a, u])}$, and
+    \[
+    \int_a^b \phi_u dG \in \overline{G(x, u]} - G(a)
+    \]
+    
+    
+    As $E^*$ is a Banach space, $G(x+)$ exists by \autoref{proposition:bounded-variation-one-side-limit}, so
+    \[
+    \mu_G([a, x]) = \lim_{u \downto x}\int_a^b \phi_u dG = \bigcap_{u > x}\overline{G((x, u])} - G(a) = G(x+) - G(a)
+    \]
+
+    
+    (1): Let $[c, d] \subset [a, b]$ such that $G$ is continuous at $c$ and $d$, then for any $x \in E$, $x \cdot \one_{[c, d]} \in RS([a, b], G)$ with
+    \[
+    \int_a^b x \cdot \one_{[c, d]} dG = x[G(d) - G(c)] = \int_{[a, b]}x \cdot \one_{[c, d]} d\mu_G
+    \]
+
+    By linearity, for any regulated step map $f: [a, b] \to E$, $\int_a^b f(t) G(dt) = \int_{[a, b]} \dpn{f(t), \mu_G(dt)}{E}$. Therefore (1) holds for $\text{Reg}([a, b], G; E)$ by the \hyperref[Linear Extension Theorem]{theorem:linear-extension-theorem-normed}. 
+\end{proof}
+
+
+% TODO: Strengthen this to the Lebesgue differentiation case in the future. 
+% It should work for ALL absolutely continuous functions. 
+
+\begin{proposition}
+\label{proposition:lebesgue-stieltjes-differentiable}
+    Let $[a, b] \subset \real$, $E$ be a normed space, $G \in C^1([a, b]; E^*)$, and $\mu_G \in M_R([a, b]; E^*)$ be the associated Lebesgue-Stieltjes measure, then
+    \[
+    \mu_G(dt) = DG(t)dt
+    \]
+\end{proposition}
+\begin{proof}
+    By the \hyperref[Fundamental Theorem of Calculus]{theorem:ftc-riemann}, for any $[c, d] \subset [a, b]$, 
+    \[
+    \int_a^b \one_{[c, d]}dG = \int_a^b \one_{[c, d]} DG(t)dt 
+    \]
+
+    By \autoref{definition:riemann-lebesgue-stieltjes}, applied to both $G$ and $\text{Id}$, 
+    \[
+    \int_{[a, b]}\one_{[c, d]}d\mu_G = \int_a^b \one_{[c, d]}dG = \int_a^b \one_{[c, d]} DG(t)dt = \int_{[a, b]} \one_{[c, d]}DG(t)dt
+    \]
+
+    Thus by linearity, for any regulated step map $f: [a, b] \to E$,
+    \[
+    \int_{[a, b]} f(t) \mu_G(dt) = \int_{[a, b]} \dpn{f(t), DG(t)}{E} dt
+    \]
+
+    By \autoref{definition:regulated-function}, the regulated step maps are dense in $\text{Reg}([a, b], G; E)$. Therefore by the \hyperref[Linear Extension Theorem]{theorem:linear-extension-theorem-normed}, the above holds for all $f \in \text{Reg}([a, b], G; E)$. By uniqueness of the \hyperref[Lebesgue-Stieltjes measure]{definition:riemann-lebesgue-stieltjes}, $\mu_G(dt) = DG(t)dt$. 
 \end{proof}
 

src/fa/rs/rs.tex

@@ -75,28 +75,4 @@
     by \autoref{lemma:sum-by-parts}, where $d$ and $Q'$ contain $\seqfz{x_j}$. Thus $(Q', d') \ge P_0$, and $\int_a^b fdG - S(Q', d', G, f) \in U$.
 \end{proof}
 
-\begin{proposition}
-\label{proposition:rs-interval}
-    Let $[a, b] \subset \real$, $E, F, H$ be TVSs over $K \in \RC$, and $E \times F \to H$ with $(x, y) \mapsto xy$ be a continuous linear map. 
-    
-    Let $G: [a, b] \to F$ and $[c, d] \subset [a, b]$ such that $G$ is continuous at $c$ and $d$, then for any $x \in E$, $x \cdot \one_{[c, d]} \in RS([a, b], G)$, and
-    \[
-    \int_a^b x \cdot \one_{[c, d]} dG = x \cdot [G(d) - G(c)]
-    \]
-\end{proposition}
-\begin{proof}
-    Assume without loss of generality that $a < c \le d < b$. Let $U \in \cn_H(0)$, then there exists $V \in \cn_F(0)$ such that $xV \subset U$. By continuity of $G$, there exists $\delta > 0$ such that $G((c - \delta, c]) - G(c) \subset V$ and $G([d, d + \delta)) - G(d) \subset V$. In which case, for any tagged partition $(P = \bracsn{x_j}_0^n, t = \seqf{t_j})$ that contains $\bracs{c - \delta, c, d, d + \delta}$, 
-    \begin{align*}
-        S(Q, t, x \cdot \one_{[c, d]}, G) &= x\sum_{a < x_j \le c - \delta}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\
-        &+ x \sum_{c - \delta < x_j \le c}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\
-        &+ x \sum_{c < x_j \le d}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j-1})] \\
-        &+ x \sum_{d < x_j \le d + \delta}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\
-        &+ x \sum_{d + \delta < x_j \le b}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\
-        &= x \sum_{c - \delta \le x_j \le c}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\
-        &+ x \cdot [G(d) - G(c)] \\
-        &+ x \sum_{d < x_j \le d + \delta}\one_{[c, d]}[G(x_j) - G(x_{j - 1})] \\
-        &\in G(d) - G(c) + xG([c - \delta, c]) + xG([d, d + \delta]) \\
-        &\subset x \cdot [G(d) - G(c)] + xV + xV \subset [G(d) - G(c)] + U + U
-    \end{align*}
-\end{proof}
 

src/topology/main/lch.tex

@@ -47,7 +47,7 @@
 
     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 \hyperref[Urysohn's lemma]{lemma:lch-urysohn}, there exists $f \in C(\ol{V}; [0, 1])$ such that $f|_K = 1$ and $f|_{\ol{W} \setminus V} = 0$. Let
+    By \hyperref[Urysohn's lemma]{lemma:urysohn}, there exists $f \in C(\ol{V}; [0, 1])$ such that $f|_K = 1$ and $f|_{\ol{W} \setminus V} = 0$. Let
     \[
     F: X \to [0, 1] \quad x \mapsto \begin{cases}
     f(x) &x \in W \\