contDiffOn_infty_iff_fderivWithin

English

On a domain with unique derivatives, ContDiffOn ∞ f s is equivalent to f being differentiable on s and fderivWithin being ContDiffOn ∞ on s.

Русский

На области с уникальными производными ContDiffOn ∞ f s эквивалентно тому, что f дифференцируема на s и fderivWithin 𝕜 f s ∈ ContDiffOn ∞ на s.

LaTeX

$$$\\text{UniqueDiffOn } 𝕜 s \\Rightarrow \\ContDiffOn 𝕜 ∞ f s \\iff \\big( \\text{DifferentiableOn } 𝕜 f s \\land \\ContDiffOn 𝕜 ∞ (fderivWithin 𝕜 f s) s \\big)$$$

Lean4

theorem contDiffOn_infty_iff_fderivWithin (hs : UniqueDiffOn 𝕜 s) :
    ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ∞ (fderivWithin 𝕜 f s) s :=
  by
  rw [← ENat.coe_top_add_one, contDiffOn_succ_iff_fderivWithin hs]
  simp

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