is_regular_diff
theoremverified
The difference L1 \\ L2 of two regular languages is regular.
Statement
theorem is_regular_diff {α : Type*} {L1 L2 : Language α} (h1 : L1.IsRegular) (h2 : L2.IsRegular) : (L1 \ L2).IsRegular
- Verified
- 07 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Used by 1
- is_regular_symm_diffThe symmetric difference of two regular languages is regular.
Lean source view module on GitHub
/-- Regular languages are closed under set difference. -/ theorem is_regular_diff {α : Type*} {L1 L2 : Language α} (h1 : L1.IsRegular) (h2 : L2.IsRegular) : (L1 \ L2).IsRegular := by rw [sdiff_eq] exact h1.inf h2.compl