Regular Closure Under Intersection

Proof idea: run the two finite automata in product, updating both states on each input symbol and accepting exactly when both component states accept. The same product construction gives intersection with a regular language as a special case.

Regular Closure Under Intersection

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

Main declarations

• Language.IsRegular.inf'
• Language.not_iff_regular_intersection

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

Regular languages are closed under intersection.

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

The converse of intersection closure fails over any nontrivial alphabet.

theorem RG_closedUnderIntersection {α : Type} [Fintype α] : ClosedUnderIntersection is_RG

The class of regular languages is closed under intersection.

theorem RG_closedUnderIntersectionWithRegular {α : Type} [Fintype α] : ClosedUnderIntersectionWithRegular is_RG

The class of regular languages is closed under intersection with regular languages.