Commit 2022-12-26 11:48 afecd239

View on Github →

feat: port Order.Copy (#1202)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Copy.lean

added def BoundedOrder.copy

added def Coframe.copy

added def CompleteDistribLattice.copy

added def CompleteLattice.copy

added def ConditionallyCompleteLattice.copy

added def DistribLattice.copy

added def Frame.copy

added def Lattice.copy