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.
Björn Brandenburg authoredddbfa9f9