contDiff_iff_contDiffAt — Mathlib

English

ContDiffAt at level 0 is equivalent to existence of a neighborhood where f is ContinuousOn.

Русский

ContDiffAt нулевого уровня эквивалентна существованию окрестности, где f непрерывна.

LaTeX

$$$ContDiffAt\ 𝕜\ 0\ f\ x\iff \exists U\ni x,\ ContinuousOn\ f\ U$$$

Lean4

theorem contDiff_iff_contDiffAt : ContDiff 𝕜 n f ↔ ∀ x, ContDiffAt 𝕜 n f x := by
  simp [← contDiffOn_univ, ContDiffOn, ContDiffAt]

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