English
If f is differentiable on an open set U and the closed ball centered at c with radius R is contained in U, then f is differentiable on the ball.
Русский
Если f дифференцируема на открытом множестве U, и шар с центром c и радиусом R целиком содержится в U, то f дифференцируема на этом шаре.
LaTeX
$$$\text{If } hf: \text{DifferentiableOn } 𝕜 f U \text{ and } \overline{B}(c,R) \subseteq U, \text{ then } \text{DiffContOnCl } 𝕜 f (\text{ball}(c,R)).$$$
Lean4
theorem diffContOnCl_ball {U : Set E} {c : E} {R : ℝ} (hf : DifferentiableOn 𝕜 f U) (hc : closedBall c R ⊆ U) :
DiffContOnCl 𝕜 f (ball c R) :=
DiffContOnCl.mk_ball (hf.mono (ball_subset_closedBall.trans hc)) (hf.continuousOn.mono hc)