Commit 2024-08-04 11:42 9b1d3da2

View on Github →

feat(WithBot): un{bot,top}_{eq,lt}_iff (#15421) this adds analogues to the existing unbot_le_iff lemmas. From the Carleson project.

Estimated changes

added theorem WithBot.eq_unbot_iff
added theorem WithBot.lt_unbot_iff
added theorem WithBot.unbot_eq_iff
added theorem WithBot.unbot_lt_iff
added theorem WithTop.eq_untop_iff
added theorem WithTop.lt_untop_iff
added theorem WithTop.untop_eq_iff
added theorem WithTop.untop_lt_iff