stable_matching_of_all_men_top_choice

theoremverified

In a marriage market market with agent types M and W, if every man m : M is matched under equivalence μ : M ≃ W to a woman μ m such that for all women w : W he does not strictly prefer w to μ m (that is, ∀ (m : M) (w : W), ¬ market.pref_m m w (μ m)), then the matching has no blocking pairs, meaning that for all m : M and w : W, ¬ (market.pref_m m w (μ m) ∧ market.pref_w w m (μ.symm w)).

Statement

theorem stable_matching_of_all_men_top_choice {M W : Type*} (market : MarriageMarket M W) (μ : M ≃ W) (h_top : ∀ (m : M) (w : W), ¬ market.pref_m m w (μ m)) : ∀ (m : M) (w : W), ¬ (market.pref_m m w (μ m) ∧ market.pref_w w m (μ.symm w))

Source

Roth & Sotomayor 1990, Section 2.2

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

Given types M and W, a marriage market market (providing preference relations market.pref_m : M → W → W → Prop and market.pref_w : W → M → M → Prop), and a bijection (equivalence) μ : M ≃ W: Assuming hypothesis h_top: for every m : M and w : W, it is not the case that market.pref_m m w (μ m) holds; Then for every 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.

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

/-- A matching in which every man receives his top choice has no blocking pairs. -/
theorem stable_matching_of_all_men_top_choice {M W : Type*} (market : MarriageMarket M W) (μ : M ≃ W) (h_top : ∀ (m : M) (w : W), ¬ market.pref_m m w (μ m)) : ∀ (m : M) (w : W), ¬ (market.pref_m m w (μ m) ∧ market.pref_w w m (μ.symm w)) := by
  intro m w ⟨h1, _⟩
  exact h_top m w h1

Discuss this result Challenge it