Commit 2024-12-02 15:59 09ceeef3

View on Github →

feat(Logic/IsEmpty): Left/Right/BiTotal truthiness on emptiness (#19555) Adds left, right, and bi_total_empty, and golfs identical_of_isEmpty in PGame as a result.

Estimated changes

Modified Mathlib/Logic/IsEmpty.lean

added theorem biTotal_empty

added theorem leftTotal_empty

added theorem rightTotal_empty

Modified Mathlib/SetTheory/Game/PGame.lean