Regular Closure Under Union

Proof idea: run the two finite automata in product, updating both states on each input symbol and accepting when either component accepts. This recognizes the union because every input is processed by both automata in lockstep.

Regular Closure Under Union

This file restates mathlib's closure of regular languages under union and shows that the converse fails over any nontrivial alphabet.

Main declarations

• Language.IsRegular.add'
• Language.not_iff_regular_union

theorem Language.IsRegular.add' {α : Type u_1} {L₁ L₂ : Language α} (h₁ : L₁.IsRegular) (h₂ : L₂.IsRegular) : (L₁ + L₂).IsRegular

Regular languages are closed under union.

theorem Language.not_iff_regular_union {α : Type u_1} [Nontrivial α] : ¬∀ (L₁ L₂ : Language α), (L₁ + L₂).IsRegular ↔ L₁.IsRegular ∧ L₂.IsRegular

The converse of union closure fails over any nontrivial alphabet.

theorem RG_closedUnderUnion {α : Type} [Fintype α] : ClosedUnderUnion is_RG

The class of regular languages is closed under union.