class_eq_co_iff_subset_co
theoremverified
A complexity class equals its complement class if and only if it is contained in its complement class.
Statement
theorem class_eq_co_iff_subset_co {α : Type*} (C : Language α → Prop) : (∀ L, C L ↔ CoClass C L) ↔ (∀ L, C L → CoClass C L)
- Source
- Sipser, Introduction to the Theory of Computation, Problem 7.27; 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.
Read back from the Lean
Given any type α and any predicate NP : Language α → Prop, the following two statements are equivalent:
1. For all languages L : Language α, NP L holds if and only if CoClass NP L holds.
2. For all languages L : Language α, if NP L holds, then CoClass NP 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 class equals its complement class iff it is contained in its complement class. -/ theorem class_eq_co_iff_subset_co {α : Type*} (C : Language α → Prop) : (∀ L, C L ↔ CoClass C L) ↔ (∀ L, C L → CoClass C L) := by constructor · intro h L exact (h L).1 · intro h L constructor · exact h L · intro hL have h1 := h Lᶜ hL dsimp [CoClass] at h1 rwa [compl_compl] at h1