is_pure_nash_equilibrium

def

In 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 player i : Player and every alternative strategy s_i' : G.Strategy i, player i's payoff from unilaterally deviating to s_i' satisfies G.payoff i (Function.update s i s_i') ≤ G.payoff i s.

Statement

def is_pure_nash_equilibrium {Player : Type*} [DecidableEq Player] (G : StrategicGame Player)
    (s : ∀ i, G.Strategy i) : Prop

Source

Nash 1951, Non-cooperative games; Osborne & Rubinstein, A Course in Game Theory, Def 14.1

Verified

07 Sep 2026

Axioms

none listed

Built on 1

StrategicGameA strategic-form game with player type Player consists of a family of strategy types Strategy i for each player i : Player, and a…

Used by 2

not_pure_nash_of_exists_better_responseIn 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…
pure_nash_of_common_payoff_maximizerIn a strategic-form game G where all players have the same payoff function u (that is, G.payoff i s = u s for every player i and strategy…

Read back from the Lean

Given a type Player with decidable equality, a strategic game G (with strategy sets G.Strategy i for each player i and payoff functions G.payoff i : (∀ j, G.Strategy j) → ℝ), and a strategy profile s : ∀ i, G.Strategy i, is_pure_nash_equilibrium G s asserts that: for every player i : Player and every alternative strategy s_i' : G.Strategy i for player i, the payoff to player i under the profile Function.update s i s_i' (where player i plays s_i' and every other player j ≠ i plays s j) is less than or equal to the payoff to player i under s.

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

/-- Predicate asserting that a pure strategy profile is a Nash equilibrium. -/
def is_pure_nash_equilibrium {Player : Type*} [DecidableEq Player] (G : StrategicGame Player)
    (s : ∀ i, G.Strategy i) : Prop :=
  ∀ (i : Player) (s_i' : G.Strategy i), G.payoff i (Function.update s i s_i') ≤ G.payoff i s

Discuss this result Challenge it