minor

blueprint/src/chapter/separating.tex

@@ -135,7 +135,7 @@ \chapter{Separating subalgebras}
 Let $\mathcal A$ be a separating subalgebra of $C_b(E, \mathbb{C})$. Let $\mu, \mu_1, \mu_2, \ldots$ be probability measures, with $(\mu_n)$ tight. If for all $f \in \mathcal A$, $\mu_n[f] \to \mu[f]$, then $\mu_n \xrightarrow{w} \mu$.
 \end{lemma}
 
-\begin{proof}\uses{lem:introduce_exponential, lem:integral_restrict_compact, lem:exponiential_M_eq_limit_M, lem:relatively_compact_of_tight}
+\begin{proof}\uses{def:separating, lem:relatively_compact_of_tight}
 To show convergence to $\mu$, it suffices to show that every subsequence has a subsequence that converges to $\mu$ (\texttt{Filter.tendsto\_of\_subseq\_tendsto}).
 Since the family is tight, it is relatively compact by Prokhorov's theorem. We get that each subsequence has a converging subsequence.
 Let then $\mu'$ be a weak limit of $\mu_n$. We have $\mu_n[f] \to \mu'[f]$ and $\mu_n[f] \to \mu[f]$ for all $f \in \mathcal A$, hence $\mu'[f] = \mu[f]$ for all $f \in \mathcal A$. Since $\mathcal A$ is separating, $\mathcal \mu' = \mu$.