is_stable_matching
def
In a marriage market with agent types M and W, a matching μ : M ≃ W is stable when no man m and woman w form a blocking pair, that is, when for every m and every w it is not the case that m prefers w to μ m and w prefers m to μ.symm w.
Statement
def is_stable_matching {M W : Type*} (market : MarriageMarket M W) (μ : M ≃ W) : Prop
- Source
- Gale & Shapley 1962, College admissions and the stability of marriage
- Verified
- 07 Sep 2026
- Axioms
- none listed
- Built on 2
- 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…
- is_blocking_pairIn a marriage market with agent types M and W and a matching μ : M ≃ W, a man m and a woman w form a blocking pair when m strictly prefers…
- Used by 2
- not_is_stable_matching_of_universal_preferenceIn the marriage market on M and W whose two preference relations are identically true, so that every agent strictly prefers everyone to…
- is_stable_matching_of_no_strict_preferenceIn the marriage market on M and W whose two preference relations are identically false, so that no agent strictly prefers anyone to…
Lean source view module on GitHub
/-- A matching is stable when no pair blocks it. -/ def is_stable_matching {M W : Type*} (market : MarriageMarket M W) (μ : M ≃ W) : Prop := ∀ (m : M) (w : W), ¬ is_blocking_pair market μ m w