Lemma (p. 121) — coordinatewise min/max of two core vectors, paired oppositely, are in the core

Proved

AssignmentGame.CoreCorners.core_lattice

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

assignment-gamecooperative-gameslatticep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $M$ (sellers) and $N$ (buyers) be finite sets and $a_{ij} \ge 0$ . Let $(u', v')$ and $(u'', v'')$ be two payoff vectors in the core, and define, for $i \in M$ and $j \in N$ ,

\underline u_i = \min(u'_i, u''_i), \quad \underline v_j = \min(v'_j, v''_j), \quad \overline u_i = \max(u'_i, u''_i), \quad \overline v_j = \max(v'_j, v''_j).

Then both

(\underline u, \overline v) \quad \text{and} \quad (\overline u, \underline v)

are in the core.

This lattice property is the heart of Theorem 3: taking sellers' minima together with buyers' maxima (or the reverse) never leaves the core.

Preamble

import Mathlib
import Definitions.Def_AssignmentGame_CoreCorners_Game

open Finset

Formal statement

namespace AssignmentGame.CoreCorners

/-- Lemma, p. 121: for two core vectors `(u', v')` and `(u'', v'')`, the vectors
`(min u' u'', max v' v'')` and `(max u' u'', min v' v'')` (taken coordinatewise) are in the
core. -/
theorem core_lattice {M N : Type*} [Fintype M] [Fintype N]
    (a : M → N → ℝ) (ha : ∀ i j, 0 ≤ a i j)
    (u' u'' : M → ℝ) (v' v'' : N → ℝ)
    (h' : (u', v') ∈ core a) (h'' : (u'', v'') ∈ core a) :
    ((fun i => min (u' i) (u'' i)), (fun j => max (v' j) (v'' j))) ∈ core a ∧
    ((fun i => max (u' i) (u'' i)), (fun j => min (v' j) (v'' j))) ∈ core a := by sorry

end AssignmentGame.CoreCorners

Source

Shapley and Shubik, The Assignment Game I: The Core, Int. J. Game Theory 1 (1971), p. 121, Lemma

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

This theorem takes arbitrary finite types $M$ and $N$ , a real matrix $a$ with $a_{ij} \ge 0$ for all $i, j$ , and two pairs $(u',v')$ and $(u'',v'')$ , where $u', u'' : M \to \mathbb{R}$ and $v', v'' : N \to \mathbb{R}$ , both lying in $\mathrm{Core}(a)$ .

Here $\mathrm{Core}(a)$ is the set of $(u,v)$ with both:

\sum_{i\in M} u_i + \sum_{j\in N} v_j = w_a(M,N)

and

\sum_{i\in A} u_i + \sum_{j\in B} v_j \ge w_a(A,B) \ \text{ for all } A\subseteq M,\ B\subseteq N.

The worth $w_a(A,B)$ is the maximum of $\sum_{(i,j)\in P} a_{ij}$ over partial matchings $P \subseteq A\times B$ , meaning no repeated seller and no repeated buyer, with the empty matching allowed.

The theorem asserts that both of these coordinatewise combinations are also in $\mathrm{Core}(a)$ :

\big(\,(\min(u'_i,u''_i))_{i\in M},\ (\max(v'_j,v''_j))_{j\in N}\,\big)

\big(\,(\max(u'_i,u''_i))_{i\in M},\ (\min(v'_j,v''_j))_{j\in N}\,\big)

In both, the minimum on one side is paired with the maximum on the other.

Degenerate cases. If $(u',v') = (u'',v'')$ , both combinations equal that same vector. If $M$ or $N$ is empty, the core is a single point, so the two given vectors coincide and the claim is immediate.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph