Progress over the past week.

src/topology/main/baire.tex

@@ -6,10 +6,10 @@
 \label{definition:baire}
     Let $X$ be a topological space, then the following are equivalent:
     \begin{enumerate}
-        \item For any $\seq{A_n}$ nowhere dense, $\bigcup_{n \in \nat}A_n \subsetneq X$.
-        \item For any $\seq{A_n}$ closed with empty interior, $\bigcup_{n \in \nat}A_n \subsetneq X$.
-        \item For any $\seq{A_n}$ closed with $\bigcup_{n \in \nat}A_n = X$, there exists $N \in \nat$ such that $\bigcup_{n \le N}A_n$ has non-empty interior.
-        \item For any $\seq{U_n}$ open and dense, $\bigcap_{n \in \nat}U_n$ is dense.
+        \item For any $\seq{A_n}$ nowhere dense, $\bigcup_{n \in \nat^+}A_n \subsetneq X$.
+        \item For any $\seq{A_n}$ closed with empty interior, $\bigcup_{n \in \nat^+}A_n \subsetneq X$.
+        \item For any $\seq{A_n}$ closed with $\bigcup_{n \in \nat^+}A_n = X$, there exists $N \in \nat^+$ such that $\bigcup_{n \le N}A_n$ has non-empty interior.
+        \item For any $\seq{U_n}$ open and dense, $\bigcap_{n \in \nat^+}U_n$ is dense.
     \end{enumerate}
     If the above holds, then $X$ is a \textbf{Baire space}.
 \end{definition}

src/topology/main/definition.tex

@@ -54,7 +54,7 @@
     Conversely, if $\cb \subset 2^X$ is a family such that:
     \begin{enumerate}
         \item[(TB1)] For every $x \in X$, there exists $U \in \cb$ such that $x \in U$.
-        \item[(TB2)] For every $x \in X$ and $U, V \in \cb$ such that $x \in U \cap$, there exists $W \in \cb$ such that $x \in W \subset U \cap V$.
+        \item[(TB2)] For every $x \in X$ and $U, V \in \cb$ such that $x \in U \cap V$, there exists $W \in \cb$ such that $x \in W \subset U \cap V$.
     \end{enumerate}
     then $\topo(\cb)$ is a topology on $X$, and $\cb$ is a base for $\topo(\cb)$.
 \end{definition}

src/topology/main/metric.tex

@@ -29,7 +29,7 @@
 
 \begin{lemma}
 \label{lemma:uniform-first-countable}
-    Let $X$ be a uniform space with a countable fundamental system of entourages, then there exists a countable fundamental system of symmetric entourages $\fB = \bracs{U_{1/2^n}|n \in \nat^+}$ such that $U_{1/2^{n+1}} \circ U_{1/2^{n+1}} \subset U_{1/2^n}$ for all $n \in \nat$.
+    Let $X$ be a uniform space with a countable fundamental system of entourages, then there exists a countable fundamental system of symmetric entourages $\fB = \bracs{U_{1/2^n}|n \in \nat^+}$ such that $U_{1/2^{n+1}} \circ U_{1/2^{n+1}} \subset U_{1/2^n}$ for all $n \in \nat^+$.
 \end{lemma}
 \begin{proof}
     Let $\seq{V}$ be a countable fundamental system of entourages. By \ref{lemma:symmetricfundamentalentourage}, there exists a symmetric entourage $U_{1/2} \subset V_1$. Suppose inductively that $U_{1/2^n}$ has been constructed, then by (U2) and \ref{lemma:symmetricfundamentalentourage}, there exists a symmetric entourage $U_{1/2^{n+1}} \subset U_{1/2^n} \cap V$. Thus $\fB = \bracs{U_{1/2^n}|n \in \nat^+}$ is the desired family.