[proofplan]
The proof has two parts. First, the tightness theorem for couplings gives tightness of $\Pi(\mu,\nu)$, and [Prokhorov's theorem](/theorems/1172) turns this tightness into relative compactness because $X \times Y$ is Polish. Second, we prove that the marginal constraints are weakly closed by testing [weak convergence](/page/Weak%20Convergence) against bounded continuous functions pulled back along the coordinate projections. A relatively compact subset that is also closed is compact.
[/proofplan]
[step:Use tightness and Prokhorov's theorem to obtain relative compactness]
Let $p_X: X \times Y \to X$ and $p_Y: X \times Y \to Y$ denote the coordinate projections. Since $X$ and $Y$ are Polish spaces, their product $X \times Y$, equipped with the [product topology](/page/Product%20Topology), is also Polish. By the tightness of the coupling set, $\Pi(\mu,\nu)$ is tight as a family of probability measures on $X \times Y$ (citing a result not yet in the wiki: Tightness of the coupling set).
Prokhorov's theorem applies on the Polish space $X \times Y$ and says that every tight family in $\mathcal{P}(X \times Y)$ is relatively compact for weak convergence (citing a result not yet in the wiki: Prokhorov theorem). Hence the weak closure
\begin{align*}
\overline{\Pi(\mu,\nu)} \subset \mathcal{P}(X \times Y)
\end{align*}
is compact.
[/step]
[step:Show that weak limits preserve the first marginal]
Let $\pi \in \overline{\Pi(\mu,\nu)}$. By definition of closure, there is a net $(\pi_\lambda)_{\lambda \in \Lambda}$ in $\Pi(\mu,\nu)$ such that $\pi_\lambda \Rightarrow \pi$ weakly in $\mathcal{P}(X \times Y)$. We prove that $(p_X)_\#\pi = \mu$.
Let $f: X \to \mathbb{R}$ be a bounded [continuous function](/page/Continuous%20Function). Define the pulled-back [test function](/page/Test%20Function)
\begin{align*}
F: X \times Y &\to \mathbb{R}, \quad F(x,y) := f(p_X(x,y)) = f(x).
\end{align*}
Since $p_X$ is continuous and $f$ is bounded and continuous, $F$ is bounded and continuous on $X \times Y$. Weak convergence of $\pi_\lambda$ to $\pi$ gives
\begin{align*}
\int_{X \times Y} F \, d\pi_\lambda \to \int_{X \times Y} F \, d\pi.
\end{align*}
For each $\lambda \in \Lambda$, the identity $(p_X)_\#\pi_\lambda = \mu$ gives, by the defining property of pushforward measures,
\begin{align*}
\int_{X \times Y} F \, d\pi_\lambda = \int_X f \, d\mu.
\end{align*}
Taking the limit in $\lambda$ therefore yields
\begin{align*}
\int_{X \times Y} F \, d\pi = \int_X f \, d\mu.
\end{align*}
Again using the defining property of the pushforward measure,
\begin{align*}
\int_X f \, d((p_X)_\#\pi) = \int_X f \, d\mu.
\end{align*}
Because bounded continuous functions determine Borel probability measures on the Polish space $X$, it follows that $(p_X)_\#\pi = \mu$.
[guided]
We want to prove that the condition on the first marginal survives passage to a weak limit. Let $\pi \in \overline{\Pi(\mu,\nu)}$. By the definition of topological closure, there exists a net $(\pi_\lambda)_{\lambda \in \Lambda}$ in $\Pi(\mu,\nu)$ such that $\pi_\lambda \Rightarrow \pi$ weakly in $\mathcal{P}(X \times Y)$. We use a net rather than a sequence so that the argument proves closedness directly in the [weak topology](/page/Weak%20Topology).
The first marginal is tested by bounded continuous functions on $X$. Let $f: X \to \mathbb{R}$ be bounded and continuous. To connect this test function on $X$ with weak convergence on $X \times Y$, pull it back along the first projection. Define
\begin{align*}
F: X \times Y &\to \mathbb{R}, \quad F(x,y) := f(p_X(x,y)) = f(x).
\end{align*}
The projection $p_X$ is continuous for the product topology, and $f$ is bounded and continuous, so $F = f \circ p_X$ is bounded and continuous on $X \times Y$. Therefore weak convergence of $\pi_\lambda$ to $\pi$ applies to this particular test function and gives
\begin{align*}
\int_{X \times Y} F \, d\pi_\lambda \to \int_{X \times Y} F \, d\pi.
\end{align*}
Now we use the fact that every $\pi_\lambda$ belongs to $\Pi(\mu,\nu)$. By definition of the coupling set, $(p_X)_\#\pi_\lambda = \mu$ for every $\lambda \in \Lambda$. The defining property of the pushforward measure says that integrating $f$ against the pushed-forward measure is the same as integrating $f \circ p_X$ against the original measure. Hence
\begin{align*}
\int_{X \times Y} F \, d\pi_\lambda = \int_X f \, d((p_X)_\#\pi_\lambda) = \int_X f \, d\mu.
\end{align*}
The left-hand side converges to $\int_{X \times Y} F \, d\pi$, while the right-hand side is independent of $\lambda$. Thus
\begin{align*}
\int_{X \times Y} F \, d\pi = \int_X f \, d\mu.
\end{align*}
Applying the pushforward identity once more, now to $\pi$, gives
\begin{align*}
\int_X f \, d((p_X)_\#\pi) = \int_X f \, d\mu.
\end{align*}
This equality holds for every bounded continuous function $f: X \to \mathbb{R}$. Since $X$ is Polish, bounded continuous functions determine Borel probability measures on $X$. Therefore $(p_X)_\#\pi = \mu$.
[/guided]
[/step]
[step:Show that weak limits preserve the second marginal]
We prove analogously that $(p_Y)_\#\pi = \nu$. Let $g: Y \to \mathbb{R}$ be a bounded continuous function, and define
\begin{align*}
G: X \times Y &\to \mathbb{R}, \quad G(x,y) := g(p_Y(x,y)) = g(y).
\end{align*}
Since $p_Y$ and $g$ are continuous and $g$ is bounded, $G$ is bounded and continuous on $X \times Y$. Weak convergence gives
\begin{align*}
\int_{X \times Y} G \, d\pi_\lambda \to \int_{X \times Y} G \, d\pi.
\end{align*}
For every $\lambda \in \Lambda$, the marginal condition $(p_Y)_\#\pi_\lambda = \nu$ gives
\begin{align*}
\int_{X \times Y} G \, d\pi_\lambda = \int_Y g \, d\nu.
\end{align*}
Passing to the limit and using the pushforward identity for $\pi$ gives
\begin{align*}
\int_Y g \, d((p_Y)_\#\pi) = \int_Y g \, d\nu.
\end{align*}
Since bounded continuous functions determine Borel probability measures on the Polish space $Y$, we conclude that $(p_Y)_\#\pi = \nu$.
[/step]
[step:Conclude that the coupling set is closed and therefore compact]
The preceding two steps show that every $\pi \in \overline{\Pi(\mu,\nu)}$ satisfies
\begin{align*}
(p_X)_\#\pi = \mu \quad \text{and} \quad (p_Y)_\#\pi = \nu.
\end{align*}
Hence $\pi \in \Pi(\mu,\nu)$, so
\begin{align*}
\overline{\Pi(\mu,\nu)} \subset \Pi(\mu,\nu).
\end{align*}
The reverse inclusion holds for every set, and therefore $\Pi(\mu,\nu)$ is weakly closed in $\mathcal{P}(X \times Y)$.
From the first step, $\overline{\Pi(\mu,\nu)}$ is compact. Since $\Pi(\mu,\nu) = \overline{\Pi(\mu,\nu)}$, the coupling set itself is compact for weak convergence in $\mathcal{P}(X \times Y)$. This proves the theorem.
[/step]