mathlib

cc65716e - refactor(analysis/complex): replace `diff_on_int_cont` with `diff_cont_on_cl` (#13148)

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.