iterate_bit1

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#Function.Involutive.iterate_bit1

English

If f is an involution, then the odd iterates yield f: f^{2n+1} = f.

Русский

Если f — инволюция, то нечётные итерации дают саму f: f^{2n+1} = f.

LaTeX

$$$\forall f: X \to X,\, \mathrm{Involutive}(f) \Rightarrow \forall n \in \mathbb{N},\, f^[2n+1] = f.$$$

Lean4

theorem iterate_bit1 (hf : Involutive f) (n : ℕ) : f^[2 * n + 1] = f := by
  rw [← succ_eq_add_one, iterate_succ, hf.iterate_bit0, id_comp]

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

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

Разделы

Аффилиация

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