CoClass

The complement class co(C) of a complexity class C on languages over alphabet α consists of all languages L whose complement is in C.

Statement

def CoClass {α : Type*} (C : Language α → Prop) : Language α → Prop

Source

Arora & Barak, Computational Complexity: A Modern Approach, Definition 2.21; Sipser, ch. 7

Verified

07 Sep 2026

Axioms

none listed

Used by 8

• class_closed_under_compl_iff_eq_coA complexity class C is closed under complement if and only if C equals its complement class co(C).
• class_eq_co_of_class_eqIf two complexity classes are equal and the first equals its complement class, then the second equals its complement class too.
• class_subset_inter_co_of_eq_coIf a complexity class equals its complement class and is contained in a second class, then it is contained in the intersection of that…
• co_class_involutiveThe complement operation on complexity classes is an involution: a language L is in co(co(C)) if and only if L is in C.
• class_eq_co_iff_subset_coA complexity class equals its complement class if and only if it is contained in its complement class.
• decider_class_eq_coAny complexity class defined by a family of deciders that is closed under negation equals its complement class.
• time_bounded_eq_co_of_decider_negation_closedLet T be a time bound and suppose the family of deciders computable within T steps is closed under Boolean negation, i.e. for every f :…
• co_class_monotoneIf a complexity class C₁ is contained in a complexity class C₂, then co(C₁) is contained in co(C₂).

Lean source view module on GitHub

/-- The complement class coC of a complexity class C consists of languages whose complement is in C. -/
def CoClass {α : Type*} (C : Language α → Prop) : Language α → Prop := fun L => C Lᶜ