mathlib3

0f6c1f19 - feat(order/conditionally_complete_lattice): conditional Inf of intervals (#7226)

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.