English
Another variant of succ_iff_hasFDerivWithinAt with a different arrangement of quantifiers and conditions.
Русский
Другая вариация succ_iff_hasFDerivWithinAt с иным расположением квантификаторов и условий.
LaTeX
$$$\text{ContDiffWithinAt}_{\mathbb{K}}(n+1,f;s;x) \iff \exists u \in 𝓝[insert x s] x, \; u \subset insert x s \land \Big( \text{AnalyticOn and HasFDerivWithinAt conditions} \Big)$$$
Lean4
/-- A function is continuously differentiable up to `n` on `s` if, for any point `x` in `s`, it
admits continuous derivatives up to order `n` on a neighborhood of `x` in `s`.
For `n = ∞`, we only require that this holds up to any finite order (where the neighborhood may
depend on the finite order we consider).
-/
@[fun_prop]
def ContDiffOn (n : WithTop ℕ∞) (f : E → F) (s : Set E) : Prop :=
∀ x ∈ s, ContDiffWithinAt 𝕜 n f s x
