not_is_stable_matching_of_universal_preference

In the marriage market on M and W whose two preference relations are identically true, so that every agent strictly prefers everyone to everyone, no matching μ : M ≃ W is stable, provided M is inhabited.

Statement

theorem not_is_stable_matching_of_universal_preference {M W : Type*}
    (m : M) (μ : M ≃ W) :
    ¬ is_stable_matching
      (MarriageMarket.mk (fun _ _ _ => True) (fun _ _ _ => True)) μ

Source

Proposed by the machine; not transcribed from the literature

Verified

07 Sep 2026

Axioms

Quot.sound

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_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

/-- Stability is not vacuous: in a market where every agent strictly prefers everyone to everyone, no matching is stable, provided there is at least one man. -/
theorem not_is_stable_matching_of_universal_preference {M W : Type*}
    (m : M) (μ : M ≃ W) :
    ¬ is_stable_matching
      (MarriageMarket.mk (fun _ _ _ => True) (fun _ _ _ => True)) μ := fun hs => hs m (μ m) ⟨trivial, trivial⟩