of_succ

Mathlib.Geometry.Manifold.ContMDiff.Defs

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

English

If ContMDiffAt for n+1 holds, then ContMDiffAt for n holds.

Русский

Если ContMDiffAt для n+1 выполняется, то выполняется и для n.

LaTeX

$$$ContMDiffAt I I' (n+1) f x \Rightarrow ContMDiffAt I I' n f x$$$

Lean4

theorem of_succ (h : ContMDiffOn I I' (n + 1) f s) : ContMDiffOn I I' n f s := fun x hx => (h x hx).of_succ

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

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

Разделы

Аффилиация

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