class_closed_under_compl_iff_eq_co
theoremverified
A complexity class C is closed under complement if and only if C equals its complement class co(C).
Statement
theorem class_closed_under_compl_iff_eq_co {α : Type*} (C : Language α → Prop) : (∀ L, C L → C Lᶜ) ↔ (∀ L, C L ↔ CoClass C L)
- Source
- Arora & Barak, Computational Complexity: A Modern Approach, Section 2.6
- 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.
- Used by 1
- decider_class_eq_coAny complexity class defined by a family of deciders that is closed under negation equals its complement class.
Read back from the Lean
For any type α and any class of languages C : Language α → Prop, C is closed under complement (that is, for every language L, if C L holds then C Lᶜ holds) if and only if for every language L, C L holds if and only if CoClass C L holds.
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
/-- A complexity class is closed under complement if and only if it equals its co-class. -/ theorem class_closed_under_compl_iff_eq_co {α : Type*} (C : Language α → Prop) : (∀ L, C L → C Lᶜ) ↔ (∀ L, C L ↔ CoClass C L) := by constructor · intro h L refine ⟨h L, fun hCo => ?_⟩ have h1 := h Lᶜ hCo rwa [compl_compl] at h1 · intro h L hCL exact (h L).mp hCL