is_blocking_pair

In 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 w to his assigned partner μ m, and w strictly prefers m to her assigned partner μ.symm w.

Statement

def is_blocking_pair {M W : Type*} (market : MarriageMarket M W)
    (μ : M ≃ W) (m : M) (w : W) : Prop

Source

Gale & Shapley 1962, College admissions and the stability of marriage

Verified

07 Sep 2026

Axioms

none listed

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…

Used by 1

• 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,…

Lean source view module on GitHub

/-- `m` and `w` block the matching `μ`: each strictly prefers the other to their assigned partner. -/
def is_blocking_pair {M W : Type*} (market : MarriageMarket M W)
    (μ : M ≃ W) (m : M) (w : W) : Prop :=
  market.pref_m m w (μ m) ∧ market.pref_w w m (μ.symm w)