Commit 2025-08-18 14:26 37129c74

View on Github →

feat(Algebra/Order): add several lemmas related to partialSups (#26851) Add 3 lemmas related to partialSups:

  • One concerns the partialSup of a function with a constant added
  • Two concern the partialSup of the succ, both of which are natural variants of the other lemma already mathlib. The lemmas couldn't be added to any of the files which already contain similar results on partialSups because in each case it would significantly increase imports.

Estimated changes

deleted theorem partialSups_add_one
added theorem partialSups_add_one'
added theorem partialSups_add_one
added theorem partialSups_succ'
added theorem map_partialSups