Commit 2024-07-03 13:56 b35dfa6d

View on Github →

feat(Order/WithBot): add forall_iff_eq_bot and forall_iff_eq_top (#14169)

Add forall_iff_eq_bot
Add forall_iff_eq_top

Estimated changes

Modified Mathlib/Data/Option/Basic.lean

added theorem Option.forall_some_ne_iff_eq_none

Modified Mathlib/Order/WithBot.lean

added theorem WithBot.forall_lt_iff_eq_bot

added theorem WithBot.forall_ne_iff_eq_bot

modified theorem WithBot.ne_bot_iff_exists

added theorem WithTop.forall_lt_iff_eq_top

added theorem WithTop.forall_ne_iff_eq_top

modified theorem WithTop.ne_top_iff_exists