involutive_iff_iter_2_eq_id

Mathlib.Logic.Function.Iterate

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

English

A function f is involutive (f∘f = id) if and only if f^{[2]} = id.

Русский

Функция f инволютивна тогда и только тогда, когда f^{[2]} = id.

LaTeX

$$$$\text{Involutive}(f) \iff f^{[2]} = \mathrm{id}.$$$$

Lean4

theorem involutive_iff_iter_2_eq_id {α} {f : α → α} : Involutive f ↔ f^[2] = id :=
  funext_iff.symm

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

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

Разделы

Аффилиация

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