condorcet_winner_unique
theoremverified
If x and y are both Condorcet winners under a preference profile P with a finite voter set V, then x = y.
Statement
theorem condorcet_winner_unique {V A : Type*} [Fintype V] (P : V → A → A → Prop) [∀ v, DecidableRel (P v)] (x y : A) (hx : condorcet_winner P x) (hy : condorcet_winner P y) : x = y
- Source
- Moulin, Axioms of Cooperative Decision Making (1988), Lemma 9.1
- Verified
- 07 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Built on 1
- condorcet_winnerIn a profile of preferences P where a finite set of voters V have pairwise preferences over alternatives A, an alternative x : A is a…
Read back from the Lean
For any finite type V and any type A, and any voter preference relation P : V → A → A → Prop (with each P v decidable), if x and y are elements of A such that both x and y are Condorcet winners under P, then x = y. That is, a Condorcet winner is unique.
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- A Condorcet winner is unique: no two distinct alternatives can both be Condorcet winners. -/ theorem condorcet_winner_unique {V A : Type*} [Fintype V] (P : V → A → A → Prop) [∀ v, DecidableRel (P v)] (x y : A) (hx : condorcet_winner P x) (hy : condorcet_winner P y) : x = y := by by_contra hne have h1 := hx y (Ne.symm hne) have h2 := hy x hne omega