rev_rev

Mathlib.Data.Fin.Fin2

URI: https://scilib.ai/kg/mathlib#Fin2.rev_rev

← MathLib Explorer

English

rev is an involution: rev(rev(i)) = i for all i ∈ Fin2 n.

Русский

rev является инволютивной функцией: rev(rev(i)) = i для любого i ∈ Fin2 n.

LaTeX

$$$\forall n,\; \mathrm{rev}\;\circ\mathrm{rev} = \mathrm{id}_{\mathrm{Fin2}(n)}$, i.e. $\forall i:\mathrm{Fin2}(n),\; \mathrm{rev}(\mathrm{rev}(i)) = i$$$

Lean4

@[simp]
theorem rev_rev {n} (i : Fin2 n) : i.rev.rev = i := by induction i <;> simp_all [rev]

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

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

Разделы

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

Аффилиация

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