reverse_one

Mathlib.Computability.Language

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

English

The reverse of the unit language is the unit language itself: reverse(1) = 1.

Русский

Обратный единичному языку язык равен самому языку: reverse(1) = 1.

LaTeX

$$reverse(1) = 1$$

Lean4

@[simp]
theorem reverse_one : (1 : Language α).reverse = 1 := by simp [reverse, ← one_def]

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

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

Разделы

Аффилиация

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