StrategicGame
structure
A strategic-form game with player type Player consists of a family of strategy types Strategy i for each player i : Player, and a real-valued payoff function payoff i : (∀ j : Player, Strategy j) → ℝ for each player i : Player.
Statement
structure StrategicGame (Player : Type*)
- Source
- Osborne & Rubinstein, A Course in Game Theory, Def 11.1; Fudenberg & Tirole, Game Theory, Def 1.1
- Verified
- 07 Sep 2026
- Axioms
- none listed
- Used by 3
- 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…
- 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
A structure StrategicGame parameterized by a type Player : Type*, consisting of:
1. Strategy: a function assigning to each player i : Player a type Strategy i of available strategies.
2. payoff: a function assigning to each player i : Player and each strategy profile (a dependent function (j : Player) → Strategy j choosing a strategy for every player) a real number ℝ representing that player's payoff.
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 strategic-form (normal-form) game with player type `Player`. -/ structure StrategicGame (Player : Type*) where Strategy : Player → Type* payoff : (i : Player) → (∀ j, Strategy j) → ℝ