diff --git a/src/measure/measure/localisable.tex b/src/measure/measure/localisable.tex index d4800c7..5712aaf 100644 --- a/src/measure/measure/localisable.tex +++ b/src/measure/measure/localisable.tex @@ -163,7 +163,7 @@ Therefore $f$ is the desired function. - Now suppose that $Y$ is an arbitrary separable metrisable space. By \autoref{lemma:admissible-approximant-existence}, there exists $\seq{I_n} \subset Y^Y$ such that: + Now suppose that $Y$ is an arbitrary separable metrisable space. By \autoref{lemma:separable-metric-space-approx-identity}, there exists $\seq{I_n} \subset Y^Y$ such that: \begin{enumerate}[label=(\roman*)] \item $I_n \to \text{Id}$ pointwise as $n \to \infty$. \item For each $n \in \natp$, $I_n(Y)$ is finite and Borel measurable.