Strictly Dominant Strategy

A strategy $s_i$ is strictly dominant for player $i$ if it strictly dominates every other strategy available to $i$:

$$\forall s'_i \neq s_i, \quad s_i \text{ strictly dominates } s'_i.$$

A strictly dominant strategy is in particular weakly dominant (Weakly Dominant Strategy); the Lean companion lemma IsStrictlyDominant.isWeaklyDominant records this and lives with Strict Dominance.

References

• [MFoGT, Section 1.3.2] Laraki, Renault, and Sorin, Mathematical Foundations of Game Theory. Strictly dominant and dominant strategies.