English
If a differentiable-on-closure condition holds on a ball and the function is continuous on the closed ball, then we have a differentiable-on-closure object on the ball.
Русский
Если выполняются условия дифференцируемости на замыкании шара и непрерывности на замкнутом шаре функции, то имеем дифференцируемость на замыкании шара.
LaTeX
$$$$\\text{If } hd:\\ DifferentiableOn\\ 𝕜\\ f\\ (ball\\ x\\ r)\\ \\text{ and } hc:\\ ContinuousOn\\ f\\ (closedBall\\ x\\ r) \\Rightarrow DiffContOnCl\\ 𝕜\\ f\\ (ball\\ x\\ r). $$$$
Lean4
theorem mk_ball {x : E} {r : ℝ} (hd : DifferentiableOn 𝕜 f (ball x r)) (hc : ContinuousOn f (closedBall x r)) :
DiffContOnCl 𝕜 f (ball x r) :=
⟨hd, hc.mono <| closure_ball_subset_closedBall⟩
