diffContOnCl_ball — Mathlib

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)

Похожие утверждения