Commit 2022-11-28 15:54 74deab33

View on Github →

feat: port Order.BoundedOrder (#697)

depends on: #642
depends on: https://github.com/leanprover-community/mathlib/pull/17730 Tracking mathlib commit: e50b8c261b0a000b806ec0e1356b41945eda61f7

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/BoundedOrder.lean

added theorem Antitone.ball

added theorem Antitone.forall

added theorem BoundedOrder.ext

added def BoundedOrder.lift

added theorem Monotone.ball

added theorem Monotone.forall

added theorem Ne.bot_lt'

added theorem Ne.bot_lt

added theorem Ne.lt_top'

added theorem Ne.lt_top

added theorem OrderBot.ext

added theorem OrderBot.ext_bot

added def OrderBot.lift

added theorem OrderDual.ofDual_bot

added theorem OrderDual.ofDual_top

added theorem OrderDual.toDual_bot

added theorem OrderDual.toDual_top

added theorem OrderTop.ext

added theorem OrderTop.ext_top

added def OrderTop.lift

added theorem Pi.bot_apply

added theorem Pi.bot_def

added theorem Pi.top_apply

added theorem Pi.top_def

added theorem StrictAnti.apply_eq_bot_iff

added theorem StrictAnti.apply_eq_top_iff

added theorem StrictMono.apply_eq_bot_iff

added theorem StrictMono.apply_eq_top_iff

added theorem StrictMono.maximal_preimage_top

added theorem StrictMono.minimal_preimage_bot

added theorem Subtype.coe_bot

added theorem Subtype.coe_eq_bot_iff

added theorem Subtype.coe_eq_top_iff

added theorem Subtype.coe_top

added theorem Subtype.mk_bot

added theorem Subtype.mk_eq_bot_iff

added theorem Subtype.mk_eq_top_iff

added theorem Subtype.mk_top

added theorem antitone_le

added theorem antitone_lt

added theorem bot_eq_false

added theorem bot_inf_eq

added theorem bot_le

added theorem bot_lt_iff_ne_bot

added theorem bot_lt_top

added theorem bot_ne_top

added theorem bot_sup_eq

added theorem bot_unique

added theorem eq_bot_iff

added theorem eq_bot_mono

added theorem eq_bot_of_bot_eq_top

added theorem eq_bot_of_minimal

added theorem eq_bot_or_bot_lt

added theorem eq_top_iff

added theorem eq_top_mono

added theorem eq_top_of_bot_eq_top

added theorem eq_top_or_lt_top

added theorem exists_ge_and_iff_exists

added theorem exists_le_and_iff_exists

added theorem inf_bot_eq

added theorem inf_eq_top_iff

added theorem inf_top_eq

added theorem isBot_bot

added theorem isBot_iff_eq_bot

added theorem isMax_iff_eq_top

added theorem isMax_top

added theorem isMin_bot

added theorem isMin_iff_eq_bot

added theorem isTop_iff_eq_top

added theorem isTop_top

added theorem le_bot_iff

added theorem le_top

added theorem lt_top_iff_ne_top

added theorem max_bot_left

added theorem max_bot_right

added theorem max_eq_bot

added theorem max_eq_top

added theorem max_top_left

added theorem max_top_right

added theorem min_bot_left

added theorem min_bot_right

added theorem min_eq_bot

added theorem min_eq_top

added theorem min_top_left

added theorem min_top_right

added theorem monotone_and

added theorem monotone_le

added theorem monotone_lt

added theorem monotone_or

added theorem ne_bot_of_gt

added theorem ne_bot_of_le_ne_bot

added theorem ne_top_of_le_ne_top

added theorem ne_top_of_lt

added theorem not_bot_lt_iff

added theorem not_isBot_iff_ne_bot

added theorem not_isMax_bot

added theorem not_isMax_iff_ne_top

added theorem not_isMin_iff_ne_bot

added theorem not_isMin_top

added theorem not_isTop_iff_ne_top

added theorem not_lt_bot

added theorem not_lt_top_iff

added theorem not_top_lt

added theorem subsingleton_iff_bot_eq_top

added theorem subsingleton_of_bot_eq_top

added theorem subsingleton_of_top_le_bot

added theorem sup_bot_eq

added theorem sup_eq_bot_iff

added theorem sup_top_eq

added theorem top_eq_true

added theorem top_inf_eq

added theorem top_le_iff

added theorem top_ne_bot

added theorem top_sup_eq

added theorem top_unique