Regular Closure Under Complement (Iff)

This file proves that a language is regular if and only if its complement is regular.

Proof idea: use the same deterministic finite automaton and replace its accept set by the Boolean complement. Since every input has a unique final DFA state, flipping acceptance recognizes exactly the complement language.

Main declarations

• Language.isRegular_compl_iff

theorem Language.isRegular_compl_iff {α : Type u_1} {L : Language α} : Lᶜ.IsRegular ↔ L.IsRegular

A language is regular if and only if its complement is regular.

theorem RG_closedUnderComplement {α : Type} [Fintype α] : ClosedUnderComplement is_RG

The class of regular languages is closed under complement.