Existence of Non-Regular Languages

This file derives the existence of a non-regular language from the concrete witness anbn and its non-regularity proof in Langlib.Classes.Regular.Examples.AnBn.

Main declarations

• exists_nonRegular_language — There exists a non-regular language over Bool.
• exists_nonRegular_language_of_nontrivial — There exists a non-regular language over any nontrivial alphabet.

theorem exists_nonRegular_language : ∃ (L : Language Bool), ¬L.IsRegular

There exists a non-regular language over Bool.

theorem exists_nonRegular_language_of_injective_bool {T : Type u_1} (f : Bool → T) (hf : Function.Injective f) : ∃ (L : Language T), ¬L.IsRegular

There exists a non-regular language over any alphabet admitting an injective coding of Bool.

theorem exists_nonRegular_language_of_pair {T : Type u_1} (a b : T) (hab : a ≠ b) : ∃ (L : Language T), ¬L.IsRegular

There exists a non-regular language over any alphabet with two distinguished symbols.

theorem exists_nonRegular_language_of_nontrivial {T : Type u_1} [Nontrivial T] : ∃ (L : Language T), ¬L.IsRegular

There exists a non-regular language over any nontrivial alphabet.

theorem exists_nonRegular_language_of_card {T : Type u_1} [Fintype T] (hT : 2 ≤ Fintype.card T) : ∃ (L : Language T), ¬L.IsRegular

There exists a non-regular language over any finite alphabet with at least two symbols.