iterate_id

Mathlib.Logic.Function.Iterate

URI: https://scilib.ai/kg/mathlib#Function.iterate_id

English

Iterating the identity map yields the identity map for all n.

Русский

Повторение тождественного отображения для любого n даёт тождественное отображение.

LaTeX

$$$$\mathrm{id}^{[n]} = \mathrm{id}$$$$

Lean4

@[simp]
theorem iterate_id (n : ℕ) : (id : α → α)^[n] = id :=
  Nat.recOn n rfl fun n ihn ↦ by rw [iterate_succ, ihn, id_comp]

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

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

Разделы

Аффилиация

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