definition
admitted
Unilateral Deviation
Given a strategy profile \(\sigma\) and a player \(i\), the unilateral deviation \((\sigma_{-i}, s'_i)\) is the profile where player \(i\) plays \(s'_i\) and all other players play according to \(\sigma\). We write \(\sigma[i \mapsto s']\).
In Lean, this is Function.update σ i s'.
References
- [MSZ, Chapter 2] Maschler, Solan, and Zamir, Game Theory. Notation for unilateral deviation.