mathlib

1521da68 - feat(order/conditionally_complete_lattice): nested intervals lemma (#4848)

feat(order/conditionally_complete_lattice): nested intervals lemma (#4848) * Add a few versions of the nested intervals lemma. * Add `pi`-instance for `conditionally_complete_lattice`.