Completeness on one side implies completeness on the other

Proved

AppliedModelingLib.Matching.Assignment.m_complete_of_w_complete_of_card_eq

by nkgarg · Sep 15, 2026 · Mathlib c5ea003 (Lean v4.30.0)

aml-gs62-stable-marriage-20260915game-theorystable-matching

Let $M$ and $W$ be finite sets with $|M|=|W|$ . A matching $\mu$ consists of optional partner maps in both directions, consistent in the sense that $\mu_M(m)=w$ if and only if $\mu_W(w)=m$ . If every member of $W$ has a partner, then

\forall m\in M,\quad \exists w\in W:\ \mu_M(m)=w.

This transfers completeness between the two sides of a balanced matching market, including the empty market.

Preamble

import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Fintype.Perm
import Mathlib.Data.Real.Basic
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_Basic

open AppliedModelingLib
open AppliedModelingLib.Matching

open AppliedModelingLib.Matching.Assignment

Formal statement

theorem AppliedModelingLib.Matching.Assignment.m_complete_of_w_complete_of_card_eq
    {M W : Type*} [Fintype M] [Fintype W] (mu : Assignment M W)
    (hcard : Fintype.card M = Fintype.card W)
    (hwComplete : ∀ w, ∃ m, mu.w_match w = some m) :
    ∀ m, ∃ w, mu.m_match m = some w := by sorry

Source

Supporting lemma in the AppliedModelingLib deferred-acceptance formalization; https://github.com/nikhgarg/AppliedModelingLib/blob/e952266be81e96bbeecea6af83d639af324a4438/AppliedModelingLib/Markets/Matching/Basic.lean#L220-L248

View graph