Commit 2024-06-04 09:29 1b66b54d

View on Github →

feat: Context-free languages are closed under reversal (#9705)

Estimated changes

Modified Mathlib/Computability/ContextFreeGrammar.lean

added theorem ContextFreeGrammar.mem_reverse_language_iff_reverse_mem_language

added def ContextFreeGrammar.reverse

added theorem ContextFreeGrammar.reverse_derives

added theorem ContextFreeGrammar.reverse_involutive

added theorem ContextFreeGrammar.reverse_mem_language_of_mem_reverse_language

added def ContextFreeRule.reverse

added theorem ContextFreeRule.reverse_involutive

added theorem Language.IsContextFree.reverse

added def Language.IsContextFree