is_stable_matching_of_no_strict_preference

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

Statement

theorem is_stable_matching_of_no_strict_preference {M W : Type*}
    (μ : M ≃ W) :
    is_stable_matching
      (MarriageMarket.mk (fun _ _ _ => False) (fun _ _ _ => False)) μ

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 satisfiable: in a market where nobody strictly prefers anyone to anyone, every matching is stable. -/
theorem is_stable_matching_of_no_strict_preference {M W : Type*}
    (μ : M ≃ W) :
    is_stable_matching
      (MarriageMarket.mk (fun _ _ _ => False) (fun _ _ _ => False)) μ := fun _ _ h => h.1