Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-22 20:53 159d9aca

View on Github →

split(order/max): Split off order.basic (#11603) This moves is_bot, is_top, no_min_order, no_max_order to a new file order.max.

Estimated changes

deleted theorem exists_gt
deleted theorem exists_lt
deleted theorem is_bot.unique
deleted def is_bot
deleted theorem is_bot_or_exists_lt
deleted theorem is_top.unique
deleted def is_top
deleted theorem is_top_or_exists_gt
deleted theorem not_is_bot
deleted theorem not_is_top
added theorem is_bot.to_dual
added theorem is_bot.unique
added def is_bot
added theorem is_bot_or_exists_lt
added theorem is_top.to_dual
added theorem is_top.unique
added def is_top
added theorem is_top_or_exists_gt
added theorem not_is_bot
added theorem not_is_top
deleted theorem is_bot.to_dual
deleted theorem is_top.to_dual