Finite languages

TheoremSingle-word languages are regular#✓fully proved

For every word \(w\) over any alphabet, the language whose only word is \(w\) is regular.

@[simp]
theorem IsRegular.singleton_word (w : List Symbol) : ({w} : Language Symbol).IsRegular

Used by 1

Used byFinite languages are regular

TheoremFinite languages are regular#✓fully proved

Every finite language over any alphabet is regular.

theorem IsRegular.of_finite {l : Language Symbol} (h : Set.Finite l) : l.IsRegular

Uses 1 · Used by 3

Proof usesSingle-word languages are regular

Used byContext-free languages are closed under inverse homomorphisms · Languages of bounded word length are regular · The reduction language of a universal language is regular

TheoremLanguages of bounded word length are regular#✓fully proved

Over a finite alphabet, if every word of a language \(L\) has length at most \(n\), for some natural number \(n\), then \(L\) is regular.

theorem IsRegular.of_length_le [Finite Symbol] {l : Language Symbol} (n : ℕ)
    (h : ∀ w ∈ l, w.length ≤ n) : l.IsRegular

Uses 1

Proof usesFinite languages are regular

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.