From 588c6ab14184cab4bb7df89def641acaafe3b7eb Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 16 Sep 2024 11:34:01 +0200
Subject: working commit

---
 library/topology/urysohn2.tex | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'library/topology/urysohn2.tex')

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}. 
-- 
cgit v1.2.3

