Functions differentiable on a domain and continuous on its closure #
Many theorems in complex analysis assume that a function is complex differentiable on a domain and
is continuous on its closure. In this file we define a predicate
DiffContOnCl that expresses
this property and prove basic facts about this predicate.
- differentiableOn : DifferentiableOn 𝕜 f s✝
A predicate saying that a function is differentiable on a set and is continuous on its closure. This is a common assumption in complex analysis.