mathlib3
0b093e6a - feat(order/bounded_lattice): a couple of basic instances about with_bot still not having a top if the original preorder didn't and vice versa (#10215)

Commit

4 years ago

feat(order/bounded_lattice): a couple of basic instances about with_bot still not having a top if the original preorder didn't and vice versa (#10215) Used in the flt-regular project.

Author

alexjbest

Parents

6af6f670

mathlib3 0b093e6a - feat(order/bounded_lattice): a couple of basic instances about with_bot still not having a top if the original preorder didn't and vice versa (#10215)

mathlib3
0b093e6a - feat(order/bounded_lattice): a couple of basic instances about with_bot still not having a top if the original preorder didn't and vice versa (#10215)