Commit 2024-11-02 09:06 f1ea505a

View on Github →

feat(ContextFreeGrammar): More lemmas about reversal (#16472) A lot of API was missing

Estimated changes

Modified Mathlib/Computability/ContextFreeGrammar.lean

added theorem ContextFreeGrammar.derives_reverse

added theorem ContextFreeGrammar.derives_reverse_comm

added theorem ContextFreeGrammar.generates_reverse

added theorem ContextFreeGrammar.generates_reverse_comm

added theorem ContextFreeGrammar.language_reverse

deleted theorem ContextFreeGrammar.mem_reverse_language_iff_reverse_mem_language

added theorem ContextFreeGrammar.produces_reverse

added theorem ContextFreeGrammar.produces_reverse_comm

modified def ContextFreeGrammar.reverse

added theorem ContextFreeGrammar.reverse_bijective

deleted theorem ContextFreeGrammar.reverse_derives

added theorem ContextFreeGrammar.reverse_injective

modified theorem ContextFreeGrammar.reverse_involutive

deleted theorem ContextFreeGrammar.reverse_mem_language_of_mem_reverse_language

added theorem ContextFreeGrammar.reverse_reverse

added theorem ContextFreeGrammar.reverse_surjective

modified theorem ContextFreeRule.Rewrites.append_left

modified theorem ContextFreeRule.Rewrites.append_right

modified theorem ContextFreeRule.Rewrites.exists_parts

added theorem ContextFreeRule.Rewrites.input_output

modified def ContextFreeRule.reverse

added theorem ContextFreeRule.reverse_bijective

added theorem ContextFreeRule.reverse_comp_reverse

added theorem ContextFreeRule.reverse_injective

modified theorem ContextFreeRule.reverse_involutive

added theorem ContextFreeRule.reverse_reverse

added theorem ContextFreeRule.reverse_surjective

modified theorem ContextFreeRule.rewrites_iff

added theorem ContextFreeRule.rewrites_reverse

added theorem ContextFreeRule.rewrites_reverse_comm

Modified Mathlib/Logic/Embedding/Basic.lean

added theorem Function.Embedding.mk_id

added theorem Function.Embedding.mk_trans_mk