mathlib3
7931ba44 - feat(order/conditionally_complete_lattice): Simp theorems (#13756)

Commit

3 years ago

feat(order/conditionally_complete_lattice): Simp theorems (#13756) We remove `supr_unit` and `infi_unit` since, thanks to #13741, they can be proven by `simp`.

Author

vihdzp

Parents

65cad418

mathlib3 7931ba44 - feat(order/conditionally_complete_lattice): Simp theorems (#13756)

mathlib3
7931ba44 - feat(order/conditionally_complete_lattice): Simp theorems (#13756)