The Riesz Representation Theorem

We formalize the Riesz-Markov-Kakutani representation theorem following pp.37-47 of the book Real and Complex Analysis by Rudin. This entry also includes formalization of regular measures, tightness of measures, and Urysohn's lemma on locally compact Hausdorff spaces. Roughly speaking, the theorem states that if $\varphi$ is a positive linear functional from $C(X)$ (the space of continuous functions from $X$ to complex numbers which have compact supports) to complex numbers, then there exists a unique measure $\mu$ such that for all $f\in C(X)$, \[\varphi(f) = \int f \mathrm{d}\mu.\]