iterate_one

Mathlib.Logic.Function.Iterate

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

English

The first iterate equals the original function: f^{[1]} = f.

Русский

Первая итерация равна самой функции: f^{[1]} = f.

LaTeX

$$$$f^{[1]} = f$$$$

Lean4

@[simp high]
theorem iterate_one : f^[1] = f :=
  funext fun _ ↦ rfl

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

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

Разделы

Аффилиация

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