Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-31 06:18 1521da68

View on Github →

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.

Estimated changes