Commit 2021-04-17 05:06 0f6c1f19
View on Github →feat(order/conditionally_complete_lattice): conditional Inf of intervals (#7226) Some new simp lemmas for cInf/cSup of intervals. I tried to use the minimal possible assumptions that I could - some lemmas are therefore in the linear order section and others are just for lattices.