Commit 2022-05-03 12:18 7931ba44

View on Github →

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.

Estimated changes

Modified src/order/conditionally_complete_lattice.lean

modified theorem infi_unique

deleted theorem infi_unit

modified theorem supr_unique

deleted theorem supr_unit