is_regular_zero
theoremverified
The empty language is regular.
Statement
theorem is_regular_zero {α : Type*} : (0 : Language α).IsRegular
- Verified
- 07 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext
Lean source view module on GitHub
/-- The empty language is regular. -/ theorem is_regular_zero {α : Type*} : (0 : Language α).IsRegular := ⟨Unit, inferInstance, ⟨fun _ _ => (), (), ∅⟩, by ext x simp [DFA.mem_accepts]⟩