reverse_reverse

Mathlib.Computability.Language

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

English

Double reversal yields the original language: reverse(reverse(l)) = l.

Русский

Двойной разворот возвращает исходный язык: reverse(reverse(l)) = l.

LaTeX

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

Lean4

@[simp]
theorem reverse_reverse (l : Language α) : l.reverse.reverse = l :=
  reverse_involutive l

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

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

Разделы

Аффилиация

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