diff --git a/src/measure/bochner-integral/strongly.tex b/src/measure/bochner-integral/strongly.tex
index d3dbdb5..c491617 100644
--- a/src/measure/bochner-integral/strongly.tex
+++ b/src/measure/bochner-integral/strongly.tex
@@ -24,7 +24,7 @@
 
     By the separable case, $f$ is $(\cm, \cb_{F})$-measurable. Let $B \in \cb_E$, then $B \cap F \in \cb_F$ by \autoref{lemma:borel-induced}. Therefore $\bracs{f \in B} = \bracs{f \in B \cap F} \in \cm$, and $f$ is $(\cm, \cb_E)$-measurable. 
 
-    (2) $\Rightarrow$ (3): By \autoref{proposition:measurable-simple-separable-norm}.
+    (2) $\Rightarrow$ (3): By \autoref{corollary:measurable-simple-separable-norm}.
 
     (3) $\Rightarrow$ (1): For each $\phi \in E^*$, $\phi \circ f = \limv{n}\phi \circ f_n$ is measurable by \autoref{proposition:limit-measurable}. Since
     \[
diff --git a/src/measure/lebesgue-integral/non-negative.tex b/src/measure/lebesgue-integral/non-negative.tex
index 45d5875..ee4d793 100644
--- a/src/measure/lebesgue-integral/non-negative.tex
+++ b/src/measure/lebesgue-integral/non-negative.tex
@@ -96,7 +96,7 @@
     Let $(X, \cm)$ be a measurable space and $f \in \mathcal{L}^+(X, \cm)$, then there exists $\seq{f_n} \subset \Sigma^+(X, \cm)$ such that $f_n \upto f$ pointwise.
 \end{lemma}
 \begin{proof}
-    By \autoref{proposition:measurable-simple-separable-norm}, there exists $\seq{g_n} \subset \Sigma^+(X, \cm)$ such that $0 \le g_n \le f$ for each $n \in \natp$, and $g_n \to f$ pointwise. For each $n \in \natp$, let $f_n = \max_{1 \le k \le n}g_k$, then $f_n \in \Sigma^+(X, \cm)$, $0 \le f_n \le f$, and $f_n \upto f$ pointwise.
+    By \autoref{corollary:measurable-simple-separable-norm}, there exists $\seq{g_n} \subset \Sigma^+(X, \cm)$ such that $0 \le g_n \le f$ for each $n \in \natp$, and $g_n \to f$ pointwise. For each $n \in \natp$, let $f_n = \max_{1 \le k \le n}g_k$, then $f_n \in \Sigma^+(X, \cm)$, $0 \le f_n \le f$, and $f_n \upto f$ pointwise.
 \end{proof}
 
 
diff --git a/src/measure/measurable-maps/metric.tex b/src/measure/measurable-maps/metric.tex
index 315f25c..cf1920b 100644
--- a/src/measure/measurable-maps/metric.tex
+++ b/src/measure/measurable-maps/metric.tex
@@ -69,41 +69,41 @@
 \end{proof}
 
 
-\begin{proposition}
-\label{proposition:measurable-simple-separable}
-    Let $(X, \cm)$ be a measurable space, $Y$ be a separable metric space, and $N: Y \to 2^Y$ such that
+\begin{lemma}
+\label{lemma:measurable-simple-separable}
+    Let $(X, \cm)$ be a measurable space, $Y$ be a separable metric space, and $\mathcal{A}: Y \to 2^Y$ such that
     \begin{enumerate}
-        \item[(a)] For each $y \in Y$, $y \in \ol{N(y)^o}$.
-        \item[(b)] $\bigcap_{y \in Y}N(y) \ne \emptyset$.
-        \item[(c)] For any $y_0 \in Y$, $\bracs{y \in Y|y_0 \in N(y)} \in \cb_Y$.
+        \item[(a)] For each $y \in Y$, $y \in \ol{\mathcal{A}(y)^o}$.
+        \item[(b)] $\bigcap_{y \in Y}\mathcal{A}(y) \ne \emptyset$.
+        \item[(c)] For any $y_0 \in Y$, $\bracs{y \in Y|y_0 \in \mathcal{A}(y)} \in \cb_Y$.
     \end{enumerate}
 
     Then, for any $f: X \to Y$, the following are equivalent:
     \begin{enumerate}
         \item $f$ is $(\cm, \cb_Y)$-measurable.
-        \item There exists a sequence $\seq{f_n}$ of $(\cm, \cb_Y)$-measurable simple functions such that
+        \item For any dense subset $\seq{y_n} \subset Y$ with $y_1 \in \bigcap_{y \in Y}\mathcal{A}(y)$, there exists a sequence $\seq{f_n}$ of $(\cm, \cb_Y)$-measurable simple functions such that
         \begin{enumerate}
-            \item[(i)] For each $x \in X$ and $n \in \natp$, $f_n(x) \in N(f(x))$.
+            \item[(i)] For each $x \in X$ and $N \in \natp$, $f_N(x) \in \mathcal{A}(f(x)) \cap \bracsn{y_n|1 \le n \le N}$.
             \item[(ii)] $f_n \to f$ pointwise.
         \end{enumerate}
 
         \item There exists a sequence $\seq{f_n}$ of $(\cm, \cb_Y)$-measurable simple functions such that $f_n \to f$ pointwise.
     \end{enumerate}
-\end{proposition}
+\end{lemma}
 \begin{proof}
-    (1) $\Rightarrow$ (2): Let $\seq{y_n} \subset Y$ be a dense subset of $Y$. Assume without loss of generality that $y_1 \in \bigcap_{y \in Y}N(y)$. For each $N \in \nat$ and $x \in X$, let
+    (1) $\Rightarrow$ (2): Let $\seq{y_n} \subset Y$ be a dense subset with $y_1 \in \bigcap_{y \in Y}\mathcal{A}(y)$. For each $N \in \natp$ and $x \in X$, define
     \[
-    C(N, x) = \bracs{1 \le n \le N|y_n \in N(f(x))}
+    C(N, x) = \bracs{1 \le n \le N|y_n \in \mathcal{A}(f(x))}
     \]
 
-    By assumption (b), $1 \in C(N, x) \ne \emptyset$. Let
+    Since $y_1 \in \bigcap_{y \in Y}\mathcal{A}(y)$, $1 \in C(N, x) \ne \emptyset$. Let
     \[
     k(N, x) = \min\bracs{n \in C(N, x) \bigg | d(f(x), y_n) = \min_{m \in C(N, x)}d(f(x), y_m)}
     \]
 
-    then for any $k \in \natp$, $\bracs{x \in X|k(n, x) \le k}$ is equal to
+    then for any $k \in \natp$, $\bracs{x \in X|k(N, x) \le k}$ is equal to
     \[
-     \bigcup_{j = 1}^k\bracs{x \in X \bigg |y_j \in C(n, x), d(f(x), y_j) = \min_{m \in C(N, x)}d(f(x), y_m)}
+     \bigcup_{j = 1}^k\bracs{x \in X \bigg |j \in C(N, x), d(f(x), y_j) = \min_{m \in C(N, x)}d(f(x), y_m)}
     \]
 
     For each $1 \le m \le N$, $y \mapsto d(y, y_m)$ is continuous. Thus $x \mapsto d(f(x), y_m)$ and $x \mapsto \min_{m \in C(N, x)}d(f(x), y_m)$ are $(\cm, \cb_\real)$-measurable by \autoref{proposition:limit-measurable} and assumption (c). By \autoref{proposition:metric-measurables},
@@ -111,44 +111,50 @@
     \bracs{x \in X \bigg | d(f(x), y_j) = \min_{m \in C(N, x)}d(f(x), y_m)} \in \cm
     \]
 
-    for each $1 \le j \le k$. Combining this with assumption (c) shows that $\bracs{x \in X|k(n, x) \le k} \in \cm$.
+    for each $1 \le j \le k$. Combining this with assumption (c) shows that $\bracs{x \in X|k(N, x) \le k} \in \cm$.
 
-    Let $f_N(x) = y_{k(N, x)}$, then for each $N \in \natp$, $f_N(x) \subset \bracs{y_n|1 \le n \le N}$, so $f_N(x)$ is finitely valued. Since $x \mapsto k{(N, x)}$ is $(\cm, 2^\nat)$-measurable, $f_N$ is $(\cm, \cb_Y)$-measurable.
+    Let $f_N(x) = y_{k(N, x)}$, then for each $N \in \natp$, $f_N(X) \subset \bracs{y_n|1 \le n \le N}$. Since $x \mapsto k{(N, x)}$ is $(\cm, 2^\natp)$-measurable, $f_N$ is $(\cm, \cb_Y)$-measurable.
 
     Fix $x \in X$, then
     \[
-    f(x) \in \ol{N^o(f(x))} = \ol{\bracs{y_n| n \in \natp, y_n \in N^o(f(x))}}
+    f(x) \in \ol{\mathcal{A}(f(x))^o} = \ol{\bracs{y_n| n \in \natp, y_n \in \mathcal{A}(f(x))^o}}
     \]
 
-    by assumption (a) and \autoref{definition:dense}. Thus for any $\eps > 0$, there exists $N \in \nat$ such that $y_N \in N^o(f(x))$ and $d(f(x), y_N) < \eps$. In which case, $d(f(x), f_n(x)) < \eps$ for all $n \ge N$. Therefore $f_n \to f$ pointwise.
+    by assumption (a) and \autoref{definition:dense}. Thus for any $\eps > 0$, there exists $N \in \natp$ such that $y_N \in \mathcal{A}(f(x))^o$ and $d(f(x), y_N) < \eps$. In which case, $d(f(x), f_n(x)) < \eps$ for all $n \ge N$. Therefore $f_n \to f$ pointwise.
 
     (3) $\Rightarrow$ (1): By \autoref{proposition:metric-measurable-limit}.
 \end{proof}
 
-\begin{proposition}
-\label{proposition:measurable-simple-separable-norm}
+\begin{corollary}
+\label{corollary:measurable-simple-separable-norm}
     Let $(X, \cm)$ be a measurable space, $(E, \norm{\cdot}_E)$ be a separable normed vector space, and $f: X \to E$, then the following are equivalent:
     \begin{enumerate}
         \item $f$ is $(\cm, \cb_E)$-measurable.
         \item There exists simple functions $\seq{f_n}$ such that $\abs{f_n} \le \abs{f}$ for all $n \in \natp$, and $f_n \to f$ pointwise.
     \end{enumerate}
-\end{proposition}
+\end{corollary}
 \begin{proof}
-    Let
+    (1) $\Rightarrow$ (2): Let
     \[
-    N: E \to 2^E \quad y \mapsto B_E(0, \norm{y}_E)
+    \mathcal{A}: E \to 2^E \quad y \mapsto \begin{cases}
+        B_E(0, \norm{y}_E) & y \ne 0 \\ 
+        E & y = 0
+    \end{cases}
     \]
 
     then
     \begin{enumerate}
-        \item[(a)] $y \in \ol{B_E(0, \norm{y}_E)}$.
-        \item[(b)] $0 \in \bigcap_{y \in E}N(y)$.
-        \item[(c)] For any fixed $y_0 \in E$,
+        \item[(a)] For each $y \in E$, $y \in \ol{\mathcal{A}(y)^o}$.
+        \item[(b)] $0 \in \bigcap_{y \in E}\mathcal{A}(y)$.
+        \item[(c)] For any fixed $y_0 \in E \setminus \bracs{0}$,
         \[
-        \bracs{y \in E|y_0 \in N(y)} = \bracs{y \in E|\norm{y_0}_E \le \norm{y}_E} \in \cb_E
+        \bracs{y \in E|y_0 \in \mathcal{A}(y)} = \bracs{y \in E|\norm{y_0}_E < \norm{y}_E} \cup \bracs{0} \in \cb_E
         \]
 
+        and $\bracs{y \in E|0 \in \mathcal{A}(y)} = E$. 
     \end{enumerate}
 
-    By \autoref{proposition:measurable-simple-separable}, (1) and (2) are equivalent.
+    By (2) of \autoref{lemma:measurable-simple-separable}, there exists simple functions $\seq{f_n}$ such that $|f_n| \le |f|$ on $\bracs{f \ne 0}$ for all $n \in \natp$ and $f_n \to f$ pointwise. In which case, $|\one_{\bracs{f \ne 0}}f_n| \le |f|$ globally for all $n \in \natp$ and $\one_{\bracs{f \ne 0}}f_n \to f$ pointwise. 
+
+    (2) $\Rightarrow$ (1): By \autoref{proposition:metric-measurable-limit}.
 \end{proof}
diff --git a/src/process/markov/definition.tex b/src/process/markov/definition.tex
index 14b0b6a..8e8982d 100644
--- a/src/process/markov/definition.tex
+++ b/src/process/markov/definition.tex
@@ -41,7 +41,7 @@
     (\bp_{s+t}\one_A)(x) = \int \one_A(y)P_{s+t}(x, dy) = \int P_t(y, A)P_s(x, dy) = \int \int \one_A(z)P_t(y, dz)P_s(x, dy)
     \]
 
-    Let $f: X \to \complex$ bounded and $(\cm, \cb_\complex)$-measurable. By \autoref{proposition:measurable-simple-separable-norm}, there exists $\seq{f_n} \subset \Sigma(X; \complex)$ such that $\abs{f_n} \le \abs{f}$ for all $n \in\nat$, and $f_n \to f$ pointwise. By the \hyperref[Dominated Convergence Theorem]{theorem:dct},
+    Let $f: X \to \complex$ bounded and $(\cm, \cb_\complex)$-measurable. By \autoref{corollary:measurable-simple-separable-norm}, there exists $\seq{f_n} \subset \Sigma(X; \complex)$ such that $\abs{f_n} \le \abs{f}$ for all $n \in\nat$, and $f_n \to f$ pointwise. By the \hyperref[Dominated Convergence Theorem]{theorem:dct},
     \begin{align*}
     (\bp_{s+t}f)(x) &= \limv{n}\int f_n(y)P_{s+t}(x, dy) = \limv{n}\iint f_n(z)P_t(y, dz)P_s(x, dy) \\
     &= \int \int f_n(z)P_t(y, dz)P_s(x, dy) = (\bp_s\bp_t) f(x)