contDiffAt — Mathlib

English

On an open set s, ContDiffOn 𝕜 n f s is equivalent to ContDiffAt 𝕜 n f a for all a in s.

Русский

На открытом множестве s ContDiffOn 𝕜 n f s эквивалентно ContDiffAt 𝕜 n f a для всех a∈s.

LaTeX

$$$\\text{IsOpen } s \\Rightarrow \\ContDiffOn 𝕜 n f s \\iff \\forall a\\,(a\\in s) \\to \\ContDiffAt 𝕜 n f a$$$

Lean4

@[fun_prop]
theorem contDiffAt (h : ContDiffOn 𝕜 n f s) (hx : s ∈ 𝓝 x) : ContDiffAt 𝕜 n f x :=
  (h _ (mem_of_mem_nhds hx)).contDiffAt hx

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