of_succ

Mathlib.Geometry.Manifold.ContMDiff.Defs

URI: https://scilib.ai/kg/mathlib#ContMDiffAt.of_succ

English

Being C^n for all natural numbers n is equivalent to being C^n for all ENat levels in the At notion.

Русский

C^n для всех целых чисел n эквивалентно C^n для всех уровней ENat в утверждении At.

LaTeX

$$$ContMDiffAt I I' ∞ f x \iff \forall n: \mathbb{N}, ContMDiffAt I I' n f x$$$

Lean4

theorem of_succ (h : ContMDiffAt I I' (n + 1) f x) : ContMDiffAt I I' n f x :=
  ContMDiffWithinAt.of_succ h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru