add lemma relating task cost and task rbf
Currently, we have lemmas stating that task_rbf
at \vareosilon
is greater than equal to task cost, and task_rbf
is monotone. I combined these two lemmas to state that tsk_rbf
at any point greater than 0
is greater than task cost. I find that this fact is regularly required in proofs and therefore, would be good to have in the facts folder.
Merge request reports
Activity
Filter activity
Please register or sign in to reply