Commit 2024-01-13 22:34 ebe630db

View on Github →

feat: add basic API lemmas for BddAbove (range f) and BddBelow (range f) (#9472) This PR adds some basic API lemmas for BddAbove (range f) (resp BddBelow). This is a ubiquitous side condition when working with iInf/iSup in conditionally complete lattices, so I think it's worth having.

Estimated changes

added theorem BddAbove.range_inv
added theorem BddAbove.range_mul
added theorem BddBelow.range_inv
added theorem BddBelow.range_mul
modified theorem ciInf_div
modified theorem ciInf_mul
modified theorem ciSup_div
modified theorem ciSup_mul
modified theorem mul_ciInf
modified theorem mul_ciSup
added theorem BddAbove.range_comp
added theorem BddAbove.range_mono
added theorem BddBelow.range_comp
added theorem BddBelow.range_mono