reverse_involutive

Mathlib.Computability.Language

URI: https://scilib.ai/kg/mathlib#Language.reverse_involutive

English

The reverse operation is an involution: reverse(reverse(l)) = l for all language l.

Русский

Операция разворота является инволютивной: reverse(reverse(L)) = L для любого языка L.

LaTeX

$$reverse(reverse(l)) = l$$

Lean4

theorem reverse_involutive : Function.Involutive (reverse : Language α → _) :=
  List.reverse_involutive.preimage

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

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

Разделы

Аффилиация

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