Language (additional definitions and theorems)

This file contains additional definitions and theorems about Language as defined and developed in Mathlib.Computability.Language.

theorem List.eq_nil_ofIsEmpty {α : Type u_1} [IsEmpty α] (xl : List α) : xl = []

[] is the only list over an empty type.

theorem Language.eq_zero_or_one_ofIsEmpty {α : Type u_1} [IsEmpty α] (l : Language α) : l = 0 ∨ l = 1

0 and 1 are the only possible languages over an empty type.

@[simp]

theorem Language.mem_biInf {α : Type u_1} {I : Type u_2} (s : Set I) (l : I → Language α) (x : List α) : x ∈ ⨅ i ∈ s, l i ↔ ∀ i ∈ s, x ∈ l i

@[simp]

theorem Language.mem_biSup {α : Type u_1} {I : Type u_2} (s : Set I) (l : I → Language α) (x : List α) : x ∈ ⨆ i ∈ s, l i ↔ ∃ i ∈ s, x ∈ l i

theorem Language.le_one_iff_eq {α : Type u_1} {l : Language α} : l ≤ 1 ↔ l = 0 ∨ l = 1

@[simp]

theorem Language.mem_singleton {α : Type u_1} (x y : List α) : x ∈ {y} ↔ x = y

@[simp]

theorem Language.mem_sub_one {α : Type u_1} {l : Language α} (x : List α) : x ∈ l - 1 ↔ x ∈ l ∧ x ≠ []

@[simp]

theorem Language.reverse_sub {α : Type u_1} (l m : Language α) : (l - m).reverse = l.reverse - m.reverse

theorem Language.sub_one_mul {α : Type u_1} {l : Language α} : (l - 1) * l = l * l - 1

theorem Language.mul_sub_one {α : Type u_1} {l : Language α} : l * (l - 1) = l * l - 1

theorem Language.kstar_sub_one {α : Type u_1} {l : Language α} : KStar.kstar l - 1 = (l - 1) * KStar.kstar l

theorem Language.sub_one_kstar {α : Type u_1} {l : Language α} : KStar.kstar (l - 1) = KStar.kstar l

theorem Language.kstar_iff_mul_add {α : Type u_1} {l m : Language α} : m = KStar.kstar l ↔ m = (l - 1) * m + 1

theorem Language.self_eq_add_mul_iff {α : Type u_1} {l m n : Language α} (hm : [] ∉ m) : l = l * m + n ↔ l = n * KStar.kstar m

The reverse version of Arden's lemma Language.self_eq_mul_add_iff.