continuousAt — Mathlib

English

If ContDiffOn 𝕜 n f s holds, then ContDiffAt 𝕜 n f x holds for any x ∈ s when considered pointwise.

Русский

Если ContDiffOn 𝕜 n f s выполняется, то ContDiffAt 𝕜 n f x выполняется для любого x∈s по точкам.

LaTeX

$$$\\forall x \\in s, \\ContDiffAt 𝕜 n f x$$$

Lean4

@[fun_prop]
theorem continuousAt (h : ContDiffAt 𝕜 n f x) : ContinuousAt f x := by
  simpa [continuousWithinAt_univ] using h.continuousWithinAt

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