Theorem top_not_mem_iff

Modification history

2025-05-25 12:30

Mathlib/Order/BoundedOrder/Basic.lean

chore(*): not_mem/nmem -> notMem (#25159)

Deleted top_not_mem_iff View on Github →

2024-08-31 20:17

Mathlib/Order/BoundedOrder.lean

feat: add `bot_not_mem_iff` for `OrderBot` (#16336)

Added top_not_mem_iff View on Github →