Regular Closure Under Reverse

Proof idea: reuse the regular-language characterization by proving regularity of L.reverse is equivalent to regularity of L. Reversing twice returns the original language, so the forward and backward directions are the same argument.

Regular Closure Under Reversal (Iff)

This file restates mathlib's proof that a language is regular if and only if its reversal is regular.

Main declarations

• Language.isRegular_reverse_iff' — local alias for the Mathlib iff statement.

theorem Language.isRegular_reverse_iff' {α : Type u_1} {L : Language α} : L.reverse.IsRegular ↔ L.IsRegular

A language is regular if and only if its reversal is regular. This is a local alias for Language.isRegular_reverse_iff from Mathlib.

theorem RG_closedUnderReverse {α : Type} [Fintype α] : ClosedUnderReverse is_RG

The class of regular languages is closed under reversal.