Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-01-18 09:14
8d5caba3
View on Github →
chore(order/bounded_order): golf (
#11538
)
Estimated changes
Modified
src/order/bounded_order.lean
modified
theorem
bot_lt_iff_ne_bot
modified
theorem
bot_unique
modified
theorem
eq_bot_iff
modified
theorem
eq_bot_mono
modified
theorem
eq_bot_of_minimal
modified
theorem
eq_bot_or_bot_lt
modified
theorem
eq_top_iff
modified
theorem
eq_top_mono
modified
theorem
eq_top_or_lt_top
modified
theorem
le_bot_iff
modified
theorem
ne_bot_of_gt
modified
theorem
ne_bot_of_le_ne_bot
modified
theorem
ne_top_of_le_ne_top
modified
theorem
ne_top_of_lt
modified
theorem
top_le_iff
modified
theorem
top_unique