working commit

1 files changed, 7 insertions, 7 deletions

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 838b121..83e3aa4 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -367,10 +367,10 @@
             \end{subproof}
             Let $N = \seq{\zero}{k}$.
             Let $M = \pow{X}$.
-            Define $V : N \to M$ such that $V(n)=$
+            Define $V : N \to M$ such that $V(n)=
             \begin{cases}
-                &\at{U}{F(n)} & \text{if} n \in N
-            \end{cases}
+                \at{U}{F(n)} & \text{if} n \in N
+            \end{cases}$
             $\dom{V} = \seq{\zero}{k}$.
             We show that $V$ is a urysohnchain of $X$.
             \begin{subproof}
@@ -445,11 +445,11 @@
     $B \subseteq X'$ by \cref{powerset_elim,closeds}.
     $A \subseteq X'$.
     Therefore $A \subseteq A'$.
-    Define $U_0: N \to \{A, A'\}$ such that $U_0(n) =$
+    Define $U_0: N \to \{A, A'\}$ such that $U_0(n) =
     \begin{cases}
-        &A  &\text{if} n = \zero \\
-        &A' &\text{if} n = 1
-    \end{cases}
+        A  &\text{if} n = \zero \\
+        A' &\text{if} n = 1
+    \end{cases}$
     $U_0$ is a function.
     $\dom{U_0} = N$.
     $\dom{U_0} \subseteq \naturals$ by \cref{ran_converse}.