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.
parent
5e60e998
No related branches found
No related tags found