English
On a domain with unique differentiability, ContDiffOn ∞ f s is equivalent to differentiability of f on s and ContDiffOn ∞ (fderivWithin 𝕜 f s) s.
Русский
На области с уникальной дифференцируемостью ContDiffOn ∞ f s эквивалентно дифференцируемости f на s и ContDiffOn ∞ (fderivWithin 𝕜 f s) s.
LaTeX
$$$\\text{UniqueDiffOn } 𝕜 s \\Rightarrow \\ContDiffOn 𝕜 ∞ f s \\iff \\big( \\text{DifferentiableOn } 𝕜 f s \\land \\ContDiffOn 𝕜 ∞ (fderivWithin 𝕜 f s) s \\big)$$$
Lean4
/-- A function is continuously differentiable up to `n` at a point `x` if, for any integer `k ≤ n`,
there is a neighborhood of `x` where `f` admits derivatives up to order `n`, which are continuous.
-/
@[fun_prop]
def ContDiffAt (n : WithTop ℕ∞) (f : E → F) (x : E) : Prop :=
ContDiffWithinAt 𝕜 n f univ x
