contDiffOn_iff — Mathlib

English

Equivalence of ContDiffOn on open sets with pointwise contDiffAt.

Русский

Эквивалентность ContDiffOn на открытых множествами со степенным ContDiffAt в точках.

LaTeX

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

Lean4

theorem contDiffOn_iff (hs : IsOpen s) : ContDiffOn 𝕜 n f s ↔ ∀ ⦃a⦄, a ∈ s → ContDiffAt 𝕜 n f a :=
  forall₂_congr fun _ => contDiffWithinAt_iff_contDiffAt ∘ hs.mem_nhds

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