Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax434930.ComplementClasses

The complexity classes coNL and coNP

concepts/Lax434930/ComplementClasses.lean · lax-434930

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Definition

    For a class C\mathcal C of binary languages, coC\mathrm{co}\mathcal C consists of languages whose complements belong to C\mathcal C. Complements are taken among all finite binary strings. In particular, A∈coNLA\in\mathrm{coNL} means A‾∈NL\overline A\in\mathrm{NL}, and A∈coNPA\in\mathrm{coNP} means A‾∈NP\overline A\in\mathrm{NP}. This operation complements each language; it does not take the set-theoretic complement of the class of languages.

    Lean source view on GitHub

    1import Lax434930.NondeterministicLogarithmicSpace
    2import Lax434930.NondeterministicPolynomialTime
    3
    4/-!
    5---
    6title: The complexity classes coNL and coNP
    7type: definition
    8---
    9For a class C\mathcal C of binary languages, coC\mathrm{co}\mathcal C
    10consists of languages whose complements belong to C\mathcal C.
    11Complements are taken among all finite binary strings. In particular,
    12A∈coNLA\in\mathrm{coNL} means A‾∈NL\overline A\in\mathrm{NL}, and
    13A∈coNPA\in\mathrm{coNP} means A‾∈NP\overline A\in\mathrm{NP}.
    14This operation complements each language; it does not take the set-theoretic
    15complement of the class of languages.
    16-/
    17
    18namespace Lax434930.ComplementClasses
    19
    20open PolynomialTime NondeterministicLogarithmicSpace NondeterministicPolynomialTime
    21
    22/-- The class of languages whose complements belong to the given class. -/
    23def co (C : Set Language) : Set Language := {A | Aᶜ ∈ C}
    24
    25/-- Complements of languages in NL. -/
    26def coNL : Set Language := co NL
    27
    28/-- Complements of languages in NP. -/
    29def coNP : Set Language := co NP
    30
    31end Lax434930.ComplementClasses
    32

    Builds on

    Used by

    From Mathlib

    none

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…