Commit 2022-11-25 17:46 4510beb3

View on Github →

feat: port Order.Lattice (#642) Tracking mathlib commit: fd47bdf09e90f553519c712378e651975fe8c829

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Subtype.lean

Modified Mathlib/Init/Algebra/Order.lean

added def maxDefault

added def minDefault

Modified Mathlib/Order/Basic.lean

Created Mathlib/Order/Lattice.lean

added theorem Antitone.le_map_inf

added theorem Antitone.map_inf

added theorem Antitone.map_sup

added theorem Antitone.map_sup_le

added def DistribLattice.ofInfSupLe

added theorem Lattice.ext

added def Lattice.mk'

added def Lattice.toLinearOrder

added theorem Monotone.forall_le_of_antitone

added theorem Monotone.le_map_sup

added theorem Monotone.map_inf

added theorem Monotone.map_inf_le

added theorem Monotone.map_sup

added theorem Monotone.of_map_inf

added theorem Monotone.of_map_sup

added theorem Ne.inf_lt_or_inf_lt

added theorem Ne.lt_sup_or_lt_sup

added theorem Pi.inf_apply

added theorem Pi.inf_def

added theorem Pi.sup_apply

added theorem Pi.sup_def

added theorem Prod.fst_inf

added theorem Prod.fst_sup

added theorem Prod.inf_def

added theorem Prod.mk_inf_mk

added theorem Prod.mk_sup_mk

added theorem Prod.snd_inf

added theorem Prod.snd_sup

added theorem Prod.sup_def

added theorem Prod.swap_inf

added theorem Prod.swap_sup

added theorem SemilatticeInf.dual_dual

added theorem SemilatticeInf.ext

added theorem SemilatticeInf.ext_inf

added def SemilatticeInf.mk'

added theorem SemilatticeSup.dual_dual

added theorem SemilatticeSup.ext

added theorem SemilatticeSup.ext_sup

added def SemilatticeSup.mk'

added theorem Subtype.coe_inf

added theorem Subtype.coe_sup

added theorem Subtype.mk_inf_mk

added theorem Subtype.mk_sup_mk

added theorem eq_of_inf_eq_sup_eq

added theorem inf_assoc

added theorem inf_comm

added theorem inf_congr_left

added theorem inf_congr_right

added theorem inf_eq_inf_iff_left

added theorem inf_eq_inf_iff_right

added theorem inf_eq_left

added theorem inf_eq_min

added theorem inf_eq_minDefault

added theorem inf_eq_right

added theorem inf_idem

added theorem inf_ind

added theorem inf_inf_distrib_left

added theorem inf_inf_distrib_right

added theorem inf_inf_inf_comm

added theorem inf_le_iff

added theorem inf_le_inf

added theorem inf_le_inf_left

added theorem inf_le_inf_right

added theorem inf_le_ite

added theorem inf_le_left'

added theorem inf_le_left

added theorem inf_le_of_left_le

added theorem inf_le_of_right_le

added theorem inf_le_right'

added theorem inf_le_right

added theorem inf_le_sup

added theorem inf_left_comm

added theorem inf_left_idem

added theorem inf_left_right_swap

added theorem inf_lt_iff

added theorem inf_lt_left

added theorem inf_lt_left_or_right

added theorem inf_lt_of_left_lt

added theorem inf_lt_of_right_lt

added theorem inf_lt_right

added theorem inf_lt_sup

added theorem inf_right_comm

added theorem inf_right_idem

added theorem inf_sup_left

added theorem inf_sup_right

added theorem inf_sup_self

added theorem ite_le_sup

added theorem le_antisymm'

added theorem le_iff_exists_sup

added theorem le_inf

added theorem le_inf_iff

added theorem le_inf_sup

added theorem le_of_inf_le_sup_le

added theorem le_sup_iff

added theorem le_sup_inf

added theorem le_sup_left'

added theorem le_sup_left

added theorem le_sup_of_le_left

added theorem le_sup_of_le_right

added theorem le_sup_right'

added theorem le_sup_right

added theorem left_eq_inf

added theorem left_eq_sup

added theorem left_lt_sup

added theorem left_or_right_lt_sup

added theorem lt_inf_iff

added theorem lt_sup_iff

added theorem lt_sup_of_lt_left

added theorem lt_sup_of_lt_right

added theorem max_max_max_comm

added theorem min_min_min_comm

added theorem ofDual_inf

added theorem ofDual_max

added theorem ofDual_min

added theorem ofDual_sup

added theorem right_eq_inf

added theorem right_eq_sup

added theorem right_lt_sup

added theorem semilatticeSup_mk'_partialOrder_eq_semilatticeInf_mk'_partialOrder

added theorem sup_assoc

added theorem sup_comm

added theorem sup_congr_left

added theorem sup_congr_right

added theorem sup_eq_iff_inf_eq

added theorem sup_eq_left

added theorem sup_eq_max

added theorem sup_eq_maxDefault

added theorem sup_eq_right

added theorem sup_eq_sup_iff_left

added theorem sup_eq_sup_iff_right

added theorem sup_idem

added theorem sup_ind

added theorem sup_inf_le

added theorem sup_inf_left

added theorem sup_inf_right

added theorem sup_inf_self

added theorem sup_le

added theorem sup_le_iff

added theorem sup_le_inf

added theorem sup_le_sup

added theorem sup_le_sup_left

added theorem sup_le_sup_right

added theorem sup_left_comm

added theorem sup_left_idem

added theorem sup_left_right_swap

added theorem sup_lt_iff

added theorem sup_right_comm

added theorem sup_right_idem

added theorem sup_sup_distrib_left

added theorem sup_sup_distrib_right

added theorem sup_sup_sup_comm

added theorem toDual_inf

added theorem toDual_max

added theorem toDual_min

added theorem toDual_sup