MarriageMarket
structure
A 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 relation pref_w : W → M → M → Prop representing women's preferences over men.
Statement
structure MarriageMarket (M W : Type*)
- Source
- Roth & Sotomayor (1990), Two-Sided Matching, Section 2.1; Gale & Shapley (1962), Section 2
- Verified
- 07 Sep 2026
- Axioms
- none listed
- Used by 7
- is_stable_matchingIn 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,…
- 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…
- 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…
- stable_matching_not_pref_of_prefIn 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…
- stable_matching_of_all_women_top_choiceIn a marriage market market with agent types M and W, if every woman w : W is matched under equivalence μ : M ≃ W to a man μ.symm w such…
- 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…
- stable_matching_of_all_men_top_choiceIn 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…
Read back from the Lean
A structure MarriageMarket parameterized by types M and W, consisting of:
1. pref_m: for each element $m : M$, a binary relation on $W$ (M → W → W → Prop), and
2. pref_w: for each element $w : W$, a binary relation on $M$ (W → M → M → Prop).
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 two-sided marriage market with agent types M and W and preference relations. -/ structure MarriageMarket (M W : Type*) where pref_m : M → W → W → Prop pref_w : W → M → M → Prop