Slices of Boolean combinations of languages

The slices of the empty and the full language (as 0 or ⊥, and ⊤), of complements, unions and intersections.

Main results

• Language.slice_zero, Language.slice_bot, Language.slice_top: slices of the empty and full languages.
• Language.slice_compl, Language.slice_sup, Language.slice_inf: slices of complements, unions, and intersections.

@[simp]

theorem Language.slice_zero {α : Type u_1} {n : ℕ} {x : Fin n → α} : slice 0 n x = false

The slices of the empty language 0 are false everywhere.

@[simp]

theorem Language.slice_bot {α : Type u_1} {n : ℕ} {x : Fin n → α} : ⊥.slice n x = false

The slices of the empty language ⊥ are false everywhere.

@[simp]

theorem Language.slice_top {α : Type u_1} {n : ℕ} {x : Fin n → α} : ⊤.slice n x = true

The slices of the full language ⊤ are true everywhere.

@[simp]

theorem Language.slice_compl {α : Type u_1} {L : Language α} {n : ℕ} {x : Fin n → α} : Lᶜ.slice n x = !L.slice n x

The slice of a complement is the negation of the slice.

@[simp]

theorem Language.slice_sup {α : Type u_1} {L M : Language α} {n : ℕ} {x : Fin n → α} : (L ⊔ M).slice n x = (L.slice n x || M.slice n x)

The slice of a union is the disjunction of the slices.

@[simp]

theorem Language.slice_inf {α : Type u_1} {L M : Language α} {n : ℕ} {x : Fin n → α} : (L ⊓ M).slice n x = (L.slice n x && M.slice n x)

The slice of an intersection is the conjunction of the slices.