continuous and differentiable on the interior

Stream: general

[Yury G. Kudryashov]

A common assumption in complex analysis is that a function is continuous on a set and is differentiable on its interior. In many cases, we apply a theorem with these assumptions to a function that is differentiable on the whole set. Then the application looks like

my_lemma hd.continuous_on (hd.mono interior_subset)

so we have to use hd twice. If we don't have hd in the environment, we need to prove it first instead of doing apply my_lemma, { ... }, { ... }.
Should we introduce a predicate

def name_me (K) (f : E → F) (s : set E) : Prop := continuous_on f s ∧ differentiable_on K f (interior s)

then provide dot notation lemmas like differentiable_on.name_me? If yes, what name would you suggest?

[Yury G. Kudryashov]

Let me suggest cont_diff_on_int. Better names are welcome.

[Sebastien Gouezel]

I'd rather avoid anything containing cont_diff, because in mathlib this now relates to higher smoothness. diff_on_int_cont would be ok, though.

[Yury G. Kudryashov]

OK.

[Yury G. Kudryashov]

Now I wonder which notion is more useful: diff_on_int_cont or diff_cont_on_cl K f s := differentiable_on K f s ∧ continuous_on f (closure s)? The latter takes an open domain as an argument.