not_pure_nash_of_exists_better_response

theoremverified

In a strategic-form game G, if some player i has an alternative strategy s_i' yielding a strictly higher payoff than at strategy profile s (that is, G.payoff i s < G.payoff i (Function.update s i s_i')), then s is not a pure Nash equilibrium.

Statement

theorem not_pure_nash_of_exists_better_response {Player : Type*} [DecidableEq Player]
    (G : StrategicGame Player) (s : ∀ i, G.Strategy i)
    (i : Player) (s_i' : G.Strategy i)
    (h : G.payoff i s < G.payoff i (Function.update s i s_i')) :
    ¬ is_pure_nash_equilibrium G s

Source

folklore

Verified

07 Sep 2026

Axioms

Classical.choiceQuot.soundpropext

Built on 2

StrategicGameA strategic-form game with player type Player consists of a family of strategy types Strategy i for each player i : Player, and a…
is_pure_nash_equilibriumIn a strategic-form game G with player type Player, a strategy profile s : ∀ i, G.Strategy i is a pure Nash equilibrium if for every…

Read back from the Lean

For any type Player with decidable equality, any strategic game G on Player, any strategy profile s : ∀ i, G.Strategy i, any player i : Player, and any alternative strategy s_i' : G.Strategy i: if player i's payoff under s is strictly less than player i's payoff under the strategy profile obtained by updating s at i to s_i' (that is, G.payoff i s < G.payoff i (Function.update s i s_i')), then s is not a pure Nash equilibrium of G.

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 strategy profile is not a pure Nash equilibrium if some player has a strictly profitable unilateral deviation. -/
theorem not_pure_nash_of_exists_better_response {Player : Type*} [DecidableEq Player]
    (G : StrategicGame Player) (s : ∀ i, G.Strategy i)
    (i : Player) (s_i' : G.Strategy i)
    (h : G.payoff i s < G.payoff i (Function.update s i s_i')) :
    ¬ is_pure_nash_equilibrium G s := fun hnash => not_le_of_gt h (hnash i s_i')

Discuss this result Challenge it