Every retained alternative precedes every rejected alternative

Proved

AppliedModelingLib.FiniteChoice.linearTopQChoice_priority

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

aml-gs62-stable-marriage-20260915college-admissionsgame-theorystable-matching

Let $A$ be any linearly ordered type with decidable equality, $q\in\mathbb N$ , and $X\subseteq A$ a finite offered set. Let $T_q(X)$ contain its first $q$ elements in increasing order, or all of $X$ when $q>|X|$ . If $x\in T_q(X)$ and $y\in X\setminus T_q(X)$ , then $x<y$ . This is the strict priority property used when a college keeps its best applicants; its college order is decreasing in the college's values. No finiteness or nonemptiness assumption is imposed on the ambient type.

Preamble

import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Lattice.Basic
import Mathlib.Data.Finset.Sort
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Prod.Lex
import Mathlib.Tactic
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_Basic
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_DeferredAcceptance
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_ManyToOne
import Definitions.Def_AMLGS62_GS62CollegeAdmissions_MainTheorems
import Definitions.Def_AMLGS62Rest_AppliedModelingLib_Foundations_Math_FiniteChoice
import Definitions.Def_AMLGS62Rest_AppliedModelingLib_Markets_Matching_ManyToOne
import Definitions.Def_AMLGS62Rest_GS62CollegeAdmissions_ExactCollegeBatchedProcedure
import Definitions.Def_AMLGS62Rest_GS62CollegeAdmissions_PaperInterface
import Definitions.Def_AMLGS62Rest_GS62CollegeAdmissions_SourceCompletion
import Definitions.Def_AMLGS62Rest_GS62CollegeAdmissions_SourceModel

open AppliedModelingLib
open AppliedModelingLib.FiniteChoice

variable {α : Type*} [DecidableEq α]

variable [LinearOrder α]

Formal statement

theorem AppliedModelingLib.FiniteChoice.linearTopQChoice_priority (q : ℕ)
    {X : Finset α} {x y : α}
    (hx : x ∈ linearTopQChoice q X)
    (hyX : y ∈ X)
    (hyNot : y ∉ linearTopQChoice q X) :
    x < y := by sorry

Source

https://github.com/nikhgarg/AppliedModelingLib/blob/e952266be81e96bbeecea6af83d639af324a4438/AppliedModelingLib/Foundations/Math/FiniteChoice.lean#L279-L327

View graph