Commit 2022-11-18 04:15 e07097c4

View on Github →

feat: port Order.Max (#567) mathlib3 hash: fd47bdf09e90f553519c712378e651975fe8c829

depends on: #566
depends on: #562

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Max.lean

added theorem IsBot.fst

added theorem IsBot.mono

added theorem IsBot.prod_mk

added theorem IsBot.snd

added def IsBot

added theorem IsMax.fst

added theorem IsMax.mono

added theorem IsMax.not_lt

added theorem IsMax.prod_mk

added theorem IsMax.snd

added def IsMax

added theorem IsMin.fst

added theorem IsMin.mono

added theorem IsMin.not_lt

added theorem IsMin.prod_mk

added theorem IsMin.snd

added def IsMin

added theorem IsTop.fst

added theorem IsTop.mono

added theorem IsTop.prod_mk

added theorem IsTop.snd

added def IsTop

added theorem NoBotOrder.to_noMinOrder

added theorem NoMaxOrder.not_acc

added theorem NoMinOrder.not_acc

added theorem NoTopOrder.to_noMaxOrder

added theorem Prod.is_bot_iff

added theorem Prod.is_max_iff

added theorem Prod.is_min_iff

added theorem Prod.is_top_iff

added theorem is_bot_of_dual_iff

added theorem is_bot_to_dual_iff

added theorem is_max_iff_forall_not_lt

added theorem is_max_of_dual_iff

added theorem is_max_to_dual_iff

added theorem is_min_iff_forall_not_lt

added theorem is_min_of_dual_iff

added theorem is_min_to_dual_iff

added theorem is_top_of_dual_iff

added theorem is_top_to_dual_iff

added theorem no_bot_order_iff_no_min_order

added theorem no_top_order_iff_no_max_order

added theorem not_is_bot

added theorem not_is_max

added theorem not_is_max_iff

added theorem not_is_max_of_lt

added theorem not_is_min

added theorem not_is_min_iff

added theorem not_is_min_of_lt

added theorem not_is_top