Read-back: stable_matching_exists

Setting and hypotheses. Let $M$ and $W$ be two finite types (both carry Fintype instances; either or both may be empty). The data are:

• $P^M$, assigning to each $m \in M$ a binary relation $P^M_m$ on $W$ (write $P^M_m(w, w')$ when the relation holds of the ordered pair $(w, w')$);
• $P^W$, assigning to each $w \in W$ a binary relation $P^W_w$ on $M$;
• hypothesis $h_M$: for every $m \in M$, the relation $P^M_m$ is a strict total order on $W$ — that is, trichotomous ($\forall w\, w'$, $P^M_m(w,w')$ or $w = w'$ or $P^M_m(w',w)$), irreflexive, and transitive;
• hypothesis $h_W$: symmetrically, for every $w \in W$, $P^W_w$ is a strict total order on $M$;
• hypothesis $h_{\mathrm{card}}$: the type of bijections $M \simeq W$ is nonempty — i.e. there merely exists some bijection between $M$ and $W$ (a Lean Equiv is a function with a two-sided inverse; the hypothesis provides no particular one). Since $M$ and $W$ are finite, this is equivalent to $|M| = |W|$.

Conclusion. There exists a bijection $\mu : M \to W$ such that no pair blocks it, i.e.

where $\mu^{-1}$ is the inverse of $\mu$. In words: there is no man–woman pair $(m,w)$ such that $m$'s relation holds of ($w$, $m$'s partner $\mu(m)$) and $w$'s relation holds of ($m$, $w$'s partner $\mu^{-1}(w)$). This unfolds the custom predicate IsStableMatching (which is exactly the "no blocking pair" condition above, and nothing more: no individual-rationality clause, no unmatched agents — $\mu$ matches everyone).

Edge cases. If $M$ and $W$ are both empty, $h_{\mathrm{card}}$ holds (the empty bijection exists), the stability condition is vacuous, and the conclusion holds trivially. If exactly one of $M, W$ is empty, $h_{\mathrm{card}}$ is false and the theorem is vacuously true for that instance. The theorem asserts mere existence ($\exists$, not $\exists!$): nothing is claimed about uniqueness or about any particular construction.