Commit 2024-08-31 20:17 e60050dd

View on Github →

feat: add bot_not_mem_iff for OrderBot (#16336)

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

added theorem one_not_mem_iff

Modified Mathlib/Order/BoundedOrder.lean

added theorem bot_not_mem_iff

added theorem top_not_mem_iff