of_succ

Mathlib.Geometry.Manifold.ContMDiff.Defs

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

English

A function is C^n for ENat∞ levels iff it is C^n for all natural numbers n

Русский

Функция C^n для всех ENat∞ эквивалентна тому, что она C^n для всех натуральных n

LaTeX

$$$ContMDiffWithinAt I I' ∞ f s x \iff ∀ n: \mathbb{N}, ContMDiffWithinAt I I' n f s x$$$

Lean4

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

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

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

Разделы

Аффилиация

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