batteries icon indicating copy to clipboard operation
batteries copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: RBSet.{upperBound?, lowerBound?} lemmas

Open digama0 opened this issue 1 year ago • 0 comments

  • [x] Depends on: #735
  • [x] Depends on: #737
  • [x] Depends on: #738

This adds RBSet.upperBound? symmetric to lowerBound?, and lifts all the RBNode theorems to RBSet (and also adds some more).

digama0 avatar Apr 14 '24 08:04 digama0