stable_matching_not_pref_of_pref
In a marriage market market with agent types M and W, if a matching equivalence μ : M ≃ W has no blocking pairs (that is, for all m : M and w : W, ¬ (market.pref_m m w (μ m) ∧ market.pref_w w m (μ.symm w))), and a man m : M strictly prefers woman w : W to his assigned partner μ m under market.pref_m, then woman w does not strictly prefer m to her assigned partner μ.symm w under market.pref_w.
Statement
theorem stable_matching_not_pref_of_pref {M W : Type*} (market : MarriageMarket M W) (μ : M ≃ W) (h_stable : ∀ (m : M) (w : W), ¬ (market.pref_m m w (μ m) ∧ market.pref_w w m (μ.symm w))) (m : M) (w : W) (h : market.pref_m m w (μ m)) : ¬ market.pref_w w m (μ.symm w)
- Source
- Roth & Sotomayor 1990, Lemma 2.8; Gale & Shapley 1962
- Verified
- 07 Sep 2026
- Axioms
Quot.sound- Built on 1
- MarriageMarketA marriage market with types M and W consists of a relation pref_m : M → W → W → Prop representing men's preferences over women, and a…
Read back from the Lean
For any types M and W, let market be a MarriageMarket M W (with preference relations pref_m : M → W → W → Prop and pref_w : W → M → M → Prop), and let μ : M ≃ W be an equivalence (bijection). Suppose that for all m : M and w : W, it is not the case that both market.pref_m m w (μ m) and market.pref_w w m (μ.symm w) hold. Then for any m : M and w : W, if market.pref_m m w (μ m) holds, it follows that market.pref_w w m (μ.symm w) does not hold (is false).
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- In a stable matching, if a man prefers another woman to his partner, that woman does not prefer him to hers. -/ theorem stable_matching_not_pref_of_pref {M W : Type*} (market : MarriageMarket M W) (μ : M ≃ W) (h_stable : ∀ (m : M) (w : W), ¬ (market.pref_m m w (μ m) ∧ market.pref_w w m (μ.symm w))) (m : M) (w : W) (h : market.pref_m m w (μ m)) : ¬ market.pref_w w m (μ.symm w) := fun hw => h_stable m w ⟨h, hw⟩