Commit 2026-09-30 00:55 3f91e898

View on Github →

chore(Order): move the definition of lattices to a new file (#44002) This PR adds a file Mathlib/Order/Defs/Lattice.lean for the definitions and basic properties of Semilattice{Inf,Sup}, Lattice and DistribLattice. This file has minimal imports, in particular, it does not import LinearOrder, so this will make it possible to have LinearOrder extend Lattice in the future. The proof in DistribLattice.ofInfSupLe (which is used by to_dual for dualizing DistribLattice.mk) had to be replaced with a manual proof because OrderDual is not imported in this file.

Estimated changes

deleted theorem eq_of_forall_le_iff
added def Lattice.mkDual
added theorem eq_of_inf_eq_sup_eq
added theorem inf_le_sup
added theorem inf_left_le_sup_left
added theorem inf_left_le_sup_right
added theorem inf_right_le_sup_right
added theorem inf_sup_le
added theorem inf_sup_left
added theorem inf_sup_right
added theorem inf_sup_self
added theorem le_of_inf_le_sup_le
added theorem le_sup_inf
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 left_eq_sup
added theorem lt_sup_of_lt_left
added theorem lt_sup_of_lt_right
added theorem right_eq_sup
added theorem sup_assoc
added theorem sup_comm
added theorem sup_eq_iff_inf_eq
added theorem sup_eq_left
added theorem sup_eq_right
added theorem sup_idem
added theorem sup_inf_le
added theorem sup_inf_left
added theorem sup_inf_right
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_right_comm
added theorem sup_right_idem
added theorem sup_rotate'
added theorem sup_rotate
added theorem sup_sup_distrib_left
added theorem sup_sup_distrib_right
added theorem sup_sup_sup_comm
added theorem eq_of_forall_le_iff
deleted def Lattice.mkDual
deleted theorem eq_of_inf_eq_sup_eq
deleted theorem inf_le_sup
deleted theorem inf_left_le_sup_left
deleted theorem inf_left_le_sup_right
deleted theorem inf_right_le_sup_right
deleted theorem inf_sup_le
deleted theorem inf_sup_left
deleted theorem inf_sup_right
deleted theorem inf_sup_self
deleted theorem le_of_inf_le_sup_le
deleted theorem le_sup_inf
deleted theorem le_sup_left
deleted theorem le_sup_of_le_left
deleted theorem le_sup_of_le_right
deleted theorem le_sup_right
deleted theorem left_eq_sup
deleted theorem lt_sup_of_lt_left
deleted theorem lt_sup_of_lt_right
deleted theorem right_eq_sup
deleted theorem sup_assoc
deleted theorem sup_comm
deleted theorem sup_eq_iff_inf_eq
deleted theorem sup_eq_left
deleted theorem sup_eq_right
deleted theorem sup_idem
deleted theorem sup_inf_le
deleted theorem sup_inf_left
deleted theorem sup_inf_right
deleted theorem sup_le
deleted theorem sup_le_iff
deleted theorem sup_le_inf
deleted theorem sup_le_sup
deleted theorem sup_le_sup_left
deleted theorem sup_le_sup_right
deleted theorem sup_left_comm
deleted theorem sup_left_idem
deleted theorem sup_left_right_swap
deleted theorem sup_right_comm
deleted theorem sup_right_idem
deleted theorem sup_rotate'
deleted theorem sup_rotate
deleted theorem sup_sup_distrib_left
deleted theorem sup_sup_distrib_right
deleted theorem sup_sup_sup_comm