Commit 2025-01-27 13:29 de461966

View on Github →

feat(Logic/IsEmpty/Relator): empty on sides (#20319) various proofs of Left/Right/BiTotal guaranteeing emptiness when certain types are empty.

Estimated changes

Modified Mathlib/Logic/IsEmpty.lean

added theorem biTotal_iff_isEmpty_left

added theorem biTotal_iff_isEmpty_right

added theorem leftTotal_iff_isEmpty_left

added theorem rightTotal_iff_isEmpty_right