contMDiffOn_of_locally_contMDiffOn

English

A function is n-times continuously differentiable at a point if it is C^n in a neighborhood in the chart.

Русский

Функция в точке x гладкая до порядка n, если в окрестности x в системе координат она принадлежит к C^n.

LaTeX

$$$ ContMDiffAt I I' n f x := ContMDiffWithinAt I I' n f univ x$$

Lean4

/-- Being `C^n` is a local property. -/
theorem contMDiffOn_of_locally_contMDiffOn (h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I' n f (s ∩ u)) :
    ContMDiffOn I I' n f s :=
  (contDiffWithinAt_localInvariantProp n).liftPropOn_of_locally_liftPropOn h

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