The singleton empty-word language is recursively enumerable

Since emptyWordLanguage T and its complement are regular, they are RE (Regular ⊆ RE). We also record that the empty language is RE.

theorem emptyWordLanguage_isRE {T : Type} [Fintype T] : is_RE (emptyWordLanguage T)

The singleton empty-word language is RE.

theorem emptyWordLanguage_compl_isRE {T : Type} [Fintype T] : is_RE (emptyWordLanguage T)ᶜ

The complement of the singleton empty-word language is RE.

theorem is_RE_empty {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] : is_RE ⊥

The empty language is RE (here we get it directly as emptyWordLanguage T ⊓ (emptyWordLanguage T)ᶜ).