Language (additional definitions and theorems)

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

@[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_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