Commit 2022-04-09 19:44 cc65716e

refactor(analysis/complex): replace diff_on_int_cont with diff_cont_on_cl (#13148) Use "differentiable on a set and continuous on its closure" instead of "continuous on a set and differentiable on its interior". There are a few reasons to prefer the latter:

• it has better "composition" lemma;
• it allows us to talk about functions that are, e.g., differentiable on {z : ℂ | abs z < 1 ∧ (re z < 0 ∨ im z ≠ 0)} and continuous on the closed unit disk. Also generalize eq_on_of_eq_on_frontier from a compact set to a bounded set (so that it works, e.g., for the unit ball in a Banach space). This PR does not move the file diff_on_int_cont to make the diff more readable; the file will be moved in another PR.