Finite labelled college seats

Definition

AMLGS62_AppliedModelingLib_Markets_Matching_ManyToOne

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

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

Let $C$ be a set of colleges and let $q:C\to\mathbb N$ assign a nonnegative integer capacity to each college. Its labelled seats form

\operatorname{Seat}(q)=\{(c,i):c\in C,\ 0\le i<q(c)\}.

If $C$ is finite, this seat set has a finite enumeration; if equality on $C$ is decidable, equality of seats is decidable. This support bundle preserves the typeclass instances of the participating source modules. The stable-marriage headline does not assert a separate college-admissions theorem.

Definition code

import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Max
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Fintype.Perm
import Mathlib.Data.Fintype.Sigma
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.Linarith

namespace AppliedModelingLib
namespace Matching

namespace ManyToOneAssignment

/-- Seat copies used to reduce a capacity-constrained college to one-to-one slots. -/
abbrev CollegeSeat {Colleges : Type*} (quota : Colleges → ℕ) :=
  Σ c, Fin (quota c)

noncomputable instance instFintypeCollegeSeat {Colleges : Type*}
    [Fintype Colleges] (quota : Colleges → ℕ) :
    Fintype (CollegeSeat quota) := by
  classical
  infer_instance

noncomputable instance instDecidableEqCollegeSeat {Colleges : Type*}
    [DecidableEq Colleges] (quota : Colleges → ℕ) :
    DecidableEq (CollegeSeat quota) := by
  classical
  infer_instance

end ManyToOneAssignment

namespace ManyToOne

end ManyToOne

end Matching
end AppliedModelingLib

Source

https://github.com/nikhgarg/AppliedModelingLib/blob/e952266be81e96bbeecea6af83d639af324a4438/AppliedModelingLib/Markets/Matching/ManyToOne.lean#L78-L97

View graph