class_subset_inter_co_of_eq_co

theoremverified

If a complexity class equals its complement class and is contained in a second class, then it is contained in the intersection of that second class with the second class's complement class.

Statement

theorem class_subset_inter_co_of_eq_co {α : Type*} (C₁ C₂ : Language α → Prop)
    (h₁ : ∀ L, C₁ L ↔ CoClass C₁ L)
    (h₂ : ∀ L, C₁ L → C₂ L) :
    ∀ L, C₁ 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 2

CoClassThe complement class co(C) of a complexity class C on languages over alphabet α consists of all languages L whose complement is in C.
co_class_monotoneIf a complexity class C₁ is contained in a complexity class C₂, then co(C₁) is contained in co(C₂).

Read back from the Lean

Given a type α, let P and NP be predicates on languages over α (i.e., complexity classes). Assume that: 1. For every language L, P holds for L if and only if CoClass P holds for L (P is closed under complement). 2. For every language L, if P holds for L, then NP holds for L (P is contained in NP). Then, for every language L, if P holds for L, then both NP holds for L and CoClass NP holds for L (i.e., L is in NP and in coNP).

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 closed under complement and contained in a second class is contained in that class intersected with its complement class. -/
theorem class_subset_inter_co_of_eq_co {α : Type*} (C₁ C₂ : Language α → Prop)
    (h₁ : ∀ L, C₁ L ↔ CoClass C₁ L)
    (h₂ : ∀ L, C₁ L → C₂ L) :
    ∀ L, C₁ L → C₂ L ∧ CoClass C₂ L := fun L hL => ⟨h₂ L hL, co_class_monotone C₁ C₂ h₂ L ((h₁ L).mp hL)⟩

Discuss this result Challenge it