class_eq_co_of_class_eq
theoremverified
If two complexity classes are equal and the first equals its complement class, then the second equals its complement class too.
Statement
theorem class_eq_co_of_class_eq {α : Type*} (C₁ C₂ : Language α → Prop) (h₁ : ∀ L, C₁ L ↔ CoClass C₁ L) (h₂ : ∀ L, C₁ L ↔ C₂ L) : ∀ L, C₂ L ↔ CoClass C₂ L
- Source
- Sipser, Introduction to the Theory of Computation, Section 7.3; 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
For any type α and any two predicates P, NP : Language α → Prop:
If:
1. For every language L, P L ↔ CoClass P L (i.e., P is closed under complement / equal to its co-class), and
2. For every language L, P L ↔ NP L (i.e., the predicates P and NP coincide on all languages),
Then:
For every language L, NP L ↔ CoClass NP L (i.e., NP is equal to its co-class).
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
/-- Equalling one's complement class transfers along equality of classes. -/ theorem class_eq_co_of_class_eq {α : Type*} (C₁ C₂ : Language α → Prop) (h₁ : ∀ L, C₁ L ↔ CoClass C₁ L) (h₂ : ∀ L, C₁ L ↔ C₂ L) : ∀ L, C₂ L ↔ CoClass C₂ L := by intro L unfold CoClass at * rw [← h₂, h₁, h₂]