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