Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-11-08 20:09
4b6c5c9c
View on Github →
feat: Sum of lattices (
#8181
) The lexicographic sum of lattices is a lattice.
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Data/Sum/Lattice.lean
added
def
Sum.Lex.inlLatticeHom
added
theorem
Sum.Lex.inl_inf
added
theorem
Sum.Lex.inl_sup
added
def
Sum.Lex.inrLatticeHom
added
theorem
Sum.Lex.inr_inf
added
theorem
Sum.Lex.inr_sup
Modified
Mathlib/Order/Disjoint.lean
added
theorem
isCompl_comm
Modified
Mathlib/Order/Synonym.lean
added
theorem
Lex.exists
added
theorem
Lex.forall