reverse_involutive

Mathlib.Computability.ContextFreeGrammar

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

English

The reverse operation on rules is an involution.

Русский

Операция разворота правил — инволюция.

LaTeX

$$$\forall r,\; Involutive(reverse)\;\text{ on } r$$$

Lean4

theorem reverse_involutive : Involutive (reverse : ContextFreeRule T N → ContextFreeRule T N) :=
  reverse_reverse

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

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

Разделы

Аффилиация

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