Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-25 06:38 17a33f0d

View on Github →

refactor(order/copy): move complete_lattice.copy to its own file (#2050)

refactor(order/copy): move complete_lattice.copy to its own file
Docstrings
Update src/order/copy.lean

Estimated changes

Modified src/data/setoid.lean

Created src/order/copy.lean

added def lattice.bounded_lattice.copy

added def lattice.complete_distrib_lattice.copy

added def lattice.complete_lattice.copy

added def lattice.conditionally_complete_lattice.copy

added def lattice.distrib_lattice.copy

Modified src/order/filter/basic.lean

deleted def lattice.complete_lattice.copy

Modified src/topology/opens.lean