co_class_involutive
theoremverified
The complement operation on complexity classes is an involution: a language L is in co(co(C)) if and only if L is in C.
Statement
theorem co_class_involutive {α : Type*} (C : Language α → Prop) (L : Language α) : CoClass (CoClass C) L ↔ C L
- Source
- Arora & Barak, Computational Complexity: A Modern Approach, ch. 2
- Verified
- 07 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Built on 1
- CoClassThe complement class co(C) of a complexity class C on languages over alphabet α consists of all languages L whose complement is in C.
Read back from the Lean
For any type α, any predicate C on languages over α, and any language L over α, L belongs to the co-class of the co-class of C if and only if L belongs to C.
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- The co-class operation is involutive: co(co(C)) = C. -/ theorem co_class_involutive {α : Type*} (C : Language α → Prop) (L : Language α) : CoClass (CoClass C) L ↔ C L := by dsimp [CoClass] rw [compl_compl]