iterate

Mathlib.Geometry.Manifold.ContMDiff.Basic

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

← MathLib Explorer

English

A constant map is ContMDiffOn.

Русский

Постоянная карта является ContMDiffOn.

LaTeX

$$$ ContMDiffOn I I' n (fun _ : M => c) s$$

Lean4

/-- The iterates of `C^n` functions on domains are `C^n`. -/
theorem iterate {f : M → M} (hf : ContMDiffOn I I n f s) (hmaps : Set.MapsTo f s s) (k : ℕ) :
    ContMDiffOn I I n (f^[k]) s := by
  induction k with
  | zero => simpa using contMDiffOn_id
  | succ k h => simpa using h.comp hf hmaps

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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