(65:V) — every solution for an acyclic relation on a finite D equals V₀

Proved

TheoryOfGames.Acyclic.eq_V0_of_isSolution

by mikedeng1 · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

cooperative-gamesorder-theoryp2o-batch-b23ap2o-gran-per-chapterp2o-plan-bookp2o-v1stable-sets

Assume the standing hypotheses of 65.7.1: $D$ is finite and $\mathcal S$ is acyclic on $D$ . Let $V_0 = B_1 \cup \cdots \cup B_{i_0-1}$ be the set of (65:2), built by the construction of 65.7.1. If $V$ is a solution (in $D$ for $\mathcal S$ ), i.e. $V = \{y \in D : x\mathcal S y \text{ for no } x \in V\}$ , then

V = V_0.

This is the uniqueness half of (65:X).

Formalization Note V0 D S is the union of all stages $B_i$ of 65.7.1, which equals $B_1 \cup \cdots \cup B_{i_0-1}$ because $B_i = \ominus$ for $i \ge i_0$ .

Preamble

import Mathlib
import Definitions.Def_TheoryOfGames_Acyclic_Solution
import Definitions.Def_TheoryOfGames_Acyclic_Acyclicity
import Definitions.Def_TheoryOfGames_Acyclic_Construction

Formal statement

namespace TheoryOfGames.Acyclic

/-- (65:V), p. 599: under the standing assumptions of 65.7.1 (`D` finite, `S` acyclic on `D`),
if `V` is a solution (in `D` for `S`), then `V = V₀`, the set of (65:2). -/
theorem eq_V0_of_isSolution {α : Type*} (D : Set α) (S : α → α → Prop)
    (hD : D.Finite) (hS : IsAcyclic D S) (V : Set α) (hV : IsSolution D S V) :
    V = V0 D S := by sorry

end TheoryOfGames.Acyclic

Source

von Neumann & Morgenstern, Theory of Games and Economic Behavior (60th-anniversary ed., Princeton 2007), p. 599, 65.7.2, (65:V)

Human review

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

View graph