Commit 2022-11-14 11:36 0e3a5421

View on Github →

feat: port Order.Basic (#556) min and max defaults are now the same between lean3 and lean4, so porting proofs in the future should be easier.

Estimated changes

Modified Mathlib/Init/Core.lean

Modified Mathlib/Order/Basic.lean

added def AsLinearOrder

modified theorem Eq.not_gt

modified theorem Eq.not_lt

added theorem Function.const_le_const

added theorem Function.const_lt_const

modified theorem LE.le.le_iff_eq

modified theorem LE.le.le_or_le

modified theorem LE.le.le_or_lt

modified theorem LE.le.lt_iff_ne

modified theorem LE.le.lt_or_le

modified theorem LT.lt.lt_or_lt

modified theorem LT.lt.ne'

added def LinearOrder.lift'

modified def LinearOrder.lift

added theorem LinearOrder.toPartialOrder_injective

deleted theorem LinearOrder.to_partial_order_injective

deleted theorem NE.le_iff_lt

deleted theorem NE.lt_of_le'

deleted theorem NE.lt_of_le

added theorem Ne.le_iff_lt

added theorem Ne.lt_of_le'

added theorem Ne.lt_of_le

added theorem Ne.lt_or_lt

added theorem Ne.not_le_or_not_le

added def Order.Preimage

deleted def Order.preimage

added theorem OrderDual.Preorder.dual_dual

added theorem OrderDual.linearOrder.dual_dual

added theorem OrderDual.partialOrder.dual_dual

added def OrderDual

added theorem PUnit.max_eq

added theorem PUnit.min_eq

added theorem PUnit.not_lt

modified def PartialOrder.lift

added theorem PartialOrder.toPreorder_injective

deleted theorem PartialOrder.to_preorder_injective

modified theorem Pi.compl_apply

modified theorem Pi.compl_def

modified theorem Pi.le_def

modified theorem Pi.lt_def

added theorem Pi.sdiff_apply

added theorem Pi.sdiff_def

modified def Preorder.lift

added theorem Preorder.toLE_injective

deleted theorem Preorder.to_le_injective

modified theorem Prod.le_def

modified theorem Prod.lt_iff

modified theorem Prod.mk_le_mk

modified theorem Prod.mk_le_mk_iff_left

modified theorem Prod.mk_le_mk_iff_right

modified theorem Prod.mk_lt_mk

modified theorem Prod.mk_lt_mk_iff_left

modified theorem Prod.mk_lt_mk_iff_right

modified theorem Prod.swap_le_swap

modified theorem Prod.swap_lt_swap

modified theorem Subtype.coe_le_coe

modified theorem Subtype.coe_lt_coe

modified theorem Subtype.mk_le_mk

modified theorem Subtype.mk_lt_mk

modified theorem dense_or_discrete

modified theorem eq_iff_le_not_lt

modified theorem eq_of_forall_ge_iff

added theorem eq_of_forall_gt_iff

modified theorem eq_of_forall_le_iff

added theorem eq_of_forall_lt_iff

added theorem eq_of_ge_of_not_gt

modified theorem eq_of_le_of_forall_ge_of_dense

modified theorem eq_of_le_of_forall_le_of_dense

added theorem eq_of_le_of_not_lt

added theorem eq_or_gt_of_le

modified theorem eq_or_lt_of_le

modified theorem exists_between

modified theorem exists_ge_of_linear

modified theorem forall_lt_iff_le'

modified theorem forall_lt_iff_le

modified theorem ge_antisymm

modified theorem ge_iff_le

modified theorem ge_of_eq

modified theorem gt_iff_lt

added theorem le_Prop_eq

modified theorem le_iff_eq_or_lt

modified theorem le_iff_le_iff_lt_iff_lt

modified theorem le_imp_le_iff_lt_imp_lt

modified theorem le_implies_le_of_le_of_le

modified theorem le_of_eq_of_le'

modified theorem le_of_eq_of_le

modified theorem le_of_forall_ge_of_dense

modified theorem le_of_forall_le'

modified theorem le_of_forall_le

modified theorem le_of_forall_le_of_dense

modified theorem le_of_forall_lt'

modified theorem le_of_forall_lt

modified theorem le_of_le_of_eq'

modified theorem le_of_le_of_eq

modified theorem le_rfl

modified theorem le_trans'

modified theorem le_update_iff

modified theorem lt_iff_le_and_ne

modified theorem lt_iff_lt_of_le_iff_le'

modified theorem lt_iff_lt_of_le_iff_le

deleted theorem lt_iff_not_ge'

added theorem lt_iff_not_le

modified theorem lt_imp_lt_of_le_imp_le

modified theorem lt_of_eq_of_lt'

modified theorem lt_of_eq_of_lt

modified theorem lt_of_le_of_lt'

modified theorem lt_of_le_of_ne'

modified theorem lt_of_lt_of_eq'

modified theorem lt_of_lt_of_eq

modified theorem lt_of_lt_of_le'

deleted theorem lt_of_not_ge'

added theorem lt_of_not_le

added theorem lt_or_lt_iff_ne

modified theorem lt_self_iff_false

modified theorem lt_trans'

added theorem max_def'

added theorem max_rec'

added theorem max_rec

added theorem min_def'

added theorem min_rec'

added theorem min_rec

deleted theorem ne.lt_or_lt

modified theorem ne_iff_lt_iff_le

added theorem ne_of_not_le

modified theorem not_le_of_lt

modified theorem not_lt_iff_eq_or_lt

modified theorem not_lt_of_le

deleted theorem order_dual.Preorder.dual_dual

deleted theorem order_dual.linear_order.dual_dual

deleted theorem order_dual.partial_order.dual_dual

deleted def order_dual

added theorem rel_imp_eq_of_rel_imp_le

added theorem subrelation_iff_le

modified theorem update_le_iff

modified theorem update_le_update_iff