condorcet_winner
In a profile of preferences P where a finite set of voters V have pairwise preferences over alternatives A, an alternative x : A is a Condorcet winner if for every alternative y ≠ x, the number of voters who strictly prefer x to y is strictly greater than the number of voters who strictly prefer y to x.
Statement
def condorcet_winner {V A : Type*} [Fintype V] (P : V → A → A → Prop) [∀ v, DecidableRel (P v)] (x : A) : Prop
- Source
- Moulin, Axioms of Cooperative Decision Making (1988), p. 228; Condorcet (1785)
- Verified
- 07 Sep 2026
- Axioms
- none listed
- Used by 1
- condorcet_winner_uniqueIf x and y are both Condorcet winners under a preference profile P with a finite voter set V, then x = y.
Read back from the Lean
Given a finite type V (of voters), a type A (of candidates/alternatives), a family of binary relations P : V → A → A → Prop where each P v is decidable, and an element x : A: x is a Condorcet winner if and only if for every y : A with y ≠ x, the number of voters v : V for which P v x y holds is strictly greater than the number of voters v : V for which P v y x holds.
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
/-- An alternative is a Condorcet winner if it strictly defeats every other alternative in pairwise majority comparison. -/ def condorcet_winner {V A : Type*} [Fintype V] (P : V → A → A → Prop) [∀ v, DecidableRel (P v)] (x : A) : Prop := ∀ y : A, y ≠ x → (Finset.filter (fun v => P v x y) Finset.univ).card > (Finset.filter (fun v => P v y x) Finset.univ).card