reverse_reverse — Mathlib

English

Applying reversal twice to a ContextFreeGrammar leaves it unchanged; the map reverse is an involution on context-free grammars.

Русский

Применение разворота два раза к контекстно-свободной грамматике оставляет её неизменной; разворот — это инволютивная отображение.

LaTeX

$$$ g^{\mathrm{reverse}\,\mathrm{reverse}} = g $$$

Lean4

@[simp]
theorem reverse_reverse (g : ContextFreeGrammar T) : g.reverse.reverse = g := by simp [reverse, Finset.map_map]

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