Commit 2023-09-28 21:41 7101b4c7

View on Github →

feat: Extend a nonnegative function (#7418) The result of extending a nonnegative function by a nonnegative function is nonnegative.

Estimated changes

added theorem Function.extend_le_one
added theorem Function.one_le_extend
added theorem dite_le_one
added theorem dite_lt_one
added theorem ite_le_one
added theorem ite_lt_one
added theorem one_le_dite
added theorem one_le_ite
added theorem one_lt_dite
added theorem one_lt_ite