Commit 2022-08-19 09:24 a07d03ac
View on Github →chore(analysis/calculus/cont_diff): Add two missing cont_diff_on lemmas (#16108)
Adds two lemmas that are immediate consequences of cont_diff_on.of_le. Names and proofs are taken verbatim from the corresponding cont_diff lemmas.