Housekeeping.

src/fa/order/order.tex

@@ -12,6 +12,30 @@
     The set $C = \bracs{x \in E|x \ge 0}$ is the \textbf{positive cone} of $E$. 
 \end{definition}
 
+\begin{definition}[Order Unit]
+\label{definition:order-unit}
+    Let $E$ be an ordered vector space and $e \in E$, then $e$ is an \textbf{order unit} if $[-e, e] \subset E$ is radial. 
+\end{definition}
+
+\begin{lemma}
+\label{lemma:order-unit-span}
+    Let $E$ be an ordered vector space with order unit $e$, then for any $x \in E$, there exists $x^+, x^- \ge 0$ such that $x = x^+ - x^-$. 
+\end{lemma}
+\begin{proof}
+    Let $\lambda > 0$ such that $\lambda e + s, \lambda e - s \ge 0$, then
+    \[
+    s = \frac{\lambda e + s}{2} - \frac{\lambda e - s}{2}
+    \]
+\end{proof}
+
+
+\begin{definition}[Archimedean]
+\label{definition:order-archimedean}
+    Let $E$ be an ordered vector space, then $E$ is \textbf{Archimedean} if for each $x \in E$, if there exists $y \in E$ such that $nx \le y$ for all $n \in \natp$, then $x \le 0$. 
+\end{definition}
+
+
+
 \begin{definition}[Ordered Topological Vector Space]
 \label{definition:ordered-tvs}
     Let $(E, \le)$ be an ordered vector space over $K \in \RC$, and $\topo$ be a vector space topology on $E$, then the triple $(E, \topo, \le)$ is an \textbf{ordered topological vector space} if the positive cone $C = \bracs{x \in E|x \ge 0}$ is closed. 

src/op/c-star/order.tex

@@ -3,7 +3,7 @@
 
 \begin{definition}[Positive]
 \label{definition:positive-c-star-algebra}
-    Let $A$ be a $C^*$-algebra and $x \in A$, then $x$ is \textbf{positive} if there exists $y \in A$ such that $x = y^*y$. 
+    Let $A$ be a $C^*$-algebra and $x \in A$, then $x$ is \textbf{positive} if there exists $y \in A$ such that $x = y^*y$. The set $A_+$ is the cone of positive elements in $A$. 
 \end{definition}
 
 \begin{proposition}

src/topology/main/definition.tex

@@ -121,6 +121,7 @@
 
 
         is a base for $\topo$.
+        \item For any topological space $Z$ and $F: Z \to X$, $F \in C(Z; X)$ if and only if $f_i \circ F \in C(Z; Y_i)$ for all $i \in I$. 
     \end{enumerate}
 
     The topology $\topo$ is the \textbf{initial/weak topology} generated by the maps $\seqi{f}$.

src/topology/main/filters.tex

@@ -133,7 +133,7 @@ The smallest filter $\fF(\fB_0) \subset 2^X$ containing $\fB_0$ is the filter \t
     (3) $\Rightarrow$ (2): $E \cup E^c = X \in \fF$.
 \end{proof}
 
-\begin{lemma}
+\begin{lemma}[Ultrafilter Lemma]
 \label{lemma:ultrafilter}
     Let $X$ be a set and $\fF \subset 2^X$, then
     \begin{enumerate}
@@ -206,3 +206,6 @@ The smallest filter $\fF(\fB_0) \subset 2^X$ containing $\fB_0$ is the filter \t
 
     is a \textbf{limit} of $f$ at $y$ with respect to $A$. If $A = X$, then $x \in A$ may be omitted.
 \end{definition}
+
+
+

src/topology/main/nets.tex

@@ -6,17 +6,87 @@
     Let $X$ be a set and $A$ be an upward-directed set, then a \textbf{net} in $X$ is a mapping $A \to X$, denoted $\net{x} \subset X$.
 \end{definition}
 
+\begin{definition}[Subnet]
+\label{definition:subnet}
+    Let $X$ be a set, $A, B$ be upward-directed sets, and $\varphi: A \to B$, then $\varphi$ is \textbf{upward-directed} if:
+    \begin{enumerate}
+        \item \textbf{(Isotone)} For any $\alpha, \beta \in A$ with $\alpha \le \beta$, $\varphi(\alpha)  \le \varphi(\beta)$. 
+        \item \textbf{(Cofinality)} For any $\beta \in B$, there exists $\alpha \in A$ such that $\varphi(\alpha) \ge \beta$. 
+    \end{enumerate}
+    
+    For any net $\angles{x_\beta}_{\beta \in B}$ and upward-directed map $\varphi: A \to B$, $\anglesn{x_{\varphi(\alpha)}}_{\alpha \in A}$ is a \textbf{subnet} of $X$. 
+\end{definition}
+
+
 \begin{definition}[Eventually]
 \label{definition:eventually}
-    Let $X$ be a set, $\net{x} \subset X$, and $E \subset X$, then $\net{x}$ is \textbf{eventually in} $E$ if there exists $\alpha_0 \in A$ such that $x_\alpha \in E$ for all $\alpha \gtrsim \alpha_0$.
+    Let $X$ be a set, $\net{x} \subset X$, and $E \subset X$, then $\net{x}$ is \textbf{eventually in} $E$ if there exists $\alpha_0 \in A$ such that $x_\alpha \in E$ for all $\alpha \ge \alpha_0$.
+
+    For any filter $\fF \subset 2^X$, $\net{x}$ is \textbf{eventually in} $\fF$ if it is eventually in $E$ for all $E \in \fF$. 
 \end{definition}
 
 \begin{definition}[Frequently]
 \label{definition:frequently}
-    Let $X$ be a set, $\net{x} \subset X$, and $E \subset X$, then $\net{x}$ is \textbf{frequently in} $E$ if for all $\alpha_0 \in A$, there exists $\alpha \gtrsim \alpha_0$ such that $x_\alpha \in E$.
+    Let $X$ be a set, $\net{x} \subset X$, and $E \subset X$, then $\net{x}$ is \textbf{frequently in} $E$ if for all $\alpha_0 \in A$, there exists $\alpha \ge \alpha_0$ such that $x_\alpha \in E$.
+
+    For any filter $\fF \subset 2^X$, $\net{x}$ is \textbf{frequently in} $\fF$ if it is frequently in $E$ for all $E \in \fF$. 
 \end{definition}
 
 \begin{definition}[Convergence]
 \label{definition:net-convergence}
     Let $X$ be a topological space and $\net{x} \subset X$, then $\net{x}$ \textbf{converges} to $x$ if for every $U \in \cn(x)$, $\net{x}$ is eventually in $U$, denoted $x_\alpha \to x$.
 \end{definition}
+
+
+\begin{definition}[Associated Net]
+\label{definition:filter-associated-net}
+    Let $X$ be a set, $\fF \subset 2^X$ be a filter, and let
+    \[
+    N_{\fF} = \bracsn{(x, F) \in X \times \fF| F \in \fF, x \in F}
+    \]
+
+    under the ordering $(x, E) \le (y, F)$ if $E \supset F$, then $N_{\fF}$ is a directed set. For each $(x, F) \in N_{\fF}$, let $x_{(x, F)} = x$, then $\angles{x_{(x, \fF)}}_{(x, \fF) \in N_{\fF}} \subset X$ is the \textbf{net associated with} $\fF$. 
+\end{definition}
+
+\begin{definition}[Tail Filter]
+\label{definition:tail-filter}
+    Let $X$ be a set and $\angles{x_\alpha}_{\alpha \in A} \subset X$ be a net. For each $\alpha \in A$, let
+    \[
+    T(\alpha) = \bracsn{x_\beta|\beta \in A, \beta \ge \alpha}
+    \]
+
+    then the filter $T_x$ generated by $\bracsn{T(\alpha)|\alpha \in A}$ is the \textbf{tail filter} of $\angles{x_\alpha}_{\alpha \in A}$. 
+\end{definition}
+
+\begin{definition}[Ultranet]
+\label{definition:ultranet}
+    Let $X$ be a set and $\angles{x_\alpha}_{\alpha \in A} \subset X$ be a net, then $\angles{x_\alpha}_{\alpha \in A}$ is an \textbf{ultranet} if for every $E \subset X$, $\angles{x_\alpha}_{\alpha \in A}$ is eventually in $E$ or $E^c$. 
+\end{definition}
+
+\begin{lemma}
+\label{lemma:filter-subnet-extraction}
+    Let $X$ be a set, $\angles{x_\alpha}_{\alpha \in A} \subset X$ be a net, and $\fF \subset 2^X$ be a filter, then the following are equivalent:
+    \begin{enumerate}
+        \item For each $F \in \fF$, $\angles{x_\alpha}_{\alpha \in A}$ is in $F$ frequently. 
+        \item There exists an subnet $\angles{x_\beta}_{\beta \in B} \subset \angles{x_\alpha}_{\alpha \in A}$ such that for each $F \in \fF$, $\angles{x_\beta}_{\beta \in B}$ is in $F$ eventually. 
+    \end{enumerate}
+\end{lemma}
+\begin{proof}
+    (1) $\Rightarrow$ (2): Let
+    \[
+    B = \bracsn{(\alpha, F) \in A \times \fF|x_\alpha \in F, F \in \fF, \alpha \in A}
+    \]
+
+    with the ordering $(\alpha, E) \ge (\beta, F)$ if $\alpha \le \beta$ and $E \supset F$, then $B$ is upward-directed. As $\angles{x_\alpha}_{\alpha \in A}$ is in $F$ frequently for all $F \in \fF$, the mapping $(\alpha, E) \mapsto \alpha$ is upward-directed. 
+    
+    For each $(x, E) \in B$, let $x_{(\alpha, E)} = x_\alpha$, then $\anglesn{x_{(\alpha, E)}}_{(\alpha,E) \in B}$ is a subnet of $\angles{x_\alpha}_{\alpha \in A}$. 
+\end{proof}
+
+\begin{lemma}
+\label{lemma:ultranet}
+    Let $X$ be a set and $\angles{x_\alpha}_{\alpha \in A} \subset X$ be a net, then $\angles{x_\alpha}_{\alpha \in A}$ admits an ultra subnet. 
+\end{lemma}
+\begin{proof}
+    Let $\fF \subset 2^X$ be the tail filter of $\angles{x_\alpha}_{\alpha \in A}$, then by the \hyperref[ultrafilter lemma]{lemma:ultrafilter}, there exists an ultrafilter $\fU \subset 2^X$ with $\fU \supset \fF$. For each $U \in \fU$, $U \cap F \ne \emptyset$ for all $F \in \fF$. Hence $\angles{x_\alpha}_{\alpha \in A}$ is frequently in $U$ for all $U \in \fU$. By \autoref{lemma:filter-subnet-extraction}, $\angles{x_\alpha}_{\alpha \in A}$ admits a subnet $\angles{x_\beta}_{\beta \in B} \subset \angles{x_\alpha}_{\alpha \in A}$ such that for each $U \in \fU$, $\angles{x_\beta}_{\beta \in B}$ is in $U$ eventually. As $\fU$ is an ultrafilter, this subnet is an ultranet. 
+\end{proof}
+