generates_reverse_comm — Mathlib

English

A grammar generates a reversed string if and only if its reverse generates the reversed string: g.reverse.Generates(u) iff g.Generates(u.reverse).

Русский

Грамматика порождает обращённую строку тогда и только тогда, когда её разворот порождает обращённую строку.

LaTeX

$$$ g.reverse.Generates(u) \iff g.Generates(u.reverse) $$$

Lean4

@[simp]
theorem generates_reverse_comm : g.reverse.Generates u ↔ g.Generates u.reverse := by simp [Generates]

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