batteries icon indicating copy to clipboard operation
batteries copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: RBMap lemmas cont'd: find?_erase

Open digama0 opened this issue 1 year ago • 0 comments

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

Continuation of the RBMap series. This adds characterizing lemmas for erase, and RBMap versions of lowerBound? and upperBound?.

digama0 avatar Apr 16 '24 15:04 digama0