contDiffWithinAt_iff_contDiffAt — Mathlib

English

If s is open, 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 \\in s, \\ContDiffAt 𝕜 n f a$$$

Lean4

theorem contDiffWithinAt_iff_contDiffAt (h : s ∈ 𝓝 x) : ContDiffWithinAt 𝕜 n f s x ↔ ContDiffAt 𝕜 n f x := by
  rw [← univ_inter s, contDiffWithinAt_inter h, contDiffWithinAt_univ]

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