co_class_monotone
theoremverifiedoriginal
If a complexity class C₁ is contained in a complexity class C₂, then co(C₁) is contained in co(C₂).
Statement
theorem co_class_monotone {α : Type*} (C₁ C₂ : Language α → Prop) (h : ∀ L, C₁ L → C₂ L) (L : Language α) (hL : CoClass C₁ L) : CoClass C₂ L
- Source
- folklore
- 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
- 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…
Read back from the Lean
For any type α, any two language classes (predicates on Language α) C₁ and C₂, and any language L : Language α, if every language satisfying C₁ also satisfies C₂, and if L is in CoClass C₁, then L is in CoClass C₂.
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
/-- The co-class operation preserves class inclusion. -/ theorem co_class_monotone {α : Type*} (C₁ C₂ : Language α → Prop) (h : ∀ L, C₁ L → C₂ L) (L : Language α) (hL : CoClass C₁ L) : CoClass C₂ L := h Lᶜ hL