mathlib

8086825f - chore(order/conditionally_complete_lattice): `with_top.coe_infi` and `with_top.coe_supr` (#15975)

chore(order/conditionally_complete_lattice): `with_top.coe_infi` and `with_top.coe_supr` (#15975) This adds `infi` and `supr` versions of the existing `Inf` and `Sup` lemmas, and adds some more general primed lemmas that work when much weaker assumptions are available on `α`.