Complements of double negation stable subtypes

Content created by Fredrik Bakke.

Created on 2025-01-07.
Last modified on 2025-01-07.

module logic.complements-double-negation-stable-subtypes where
Imports 
open import foundation.dependent-pair-types
open import foundation.double-negation
open import foundation.double-negation-stable-propositions
open import foundation.full-subtypes
open import foundation.involutions
open import foundation.negation
open import foundation.postcomposition-functions
open import foundation.powersets
open import foundation.propositional-truncations
open import foundation.subtypes
open import foundation.unions-subtypes
open import foundation.universe-levels

open import foundation-core.function-types

open import logic.double-negation-stable-subtypes

Idea

The complement of a double negation stable subtype B ⊆ A consists of the elements that are not in B.

Definition

Complements of double negation stable subtypes

complement-double-negation-stable-subtype :
  {l1 l2 : Level} {A : UU l1} →
  double-negation-stable-subtype l2 A →
  double-negation-stable-subtype l2 A
complement-double-negation-stable-subtype P x =
  neg-Double-Negation-Stable-Prop (P x)

Properties

Taking complements is an involution on double negation stable subtypes

is-involution-complement-double-negation-stable-subtype :
  {l1 l2 : Level} {A : UU l1} →
  is-involution (complement-double-negation-stable-subtype {l1} {l2} {A})
is-involution-complement-double-negation-stable-subtype P =
  eq-has-same-elements-double-negation-stable-subtype
    ( complement-double-negation-stable-subtype
      ( complement-double-negation-stable-subtype P))
    ( P)
    ( λ x →
      ( is-double-negation-stable-double-negation-stable-subtype P x ,
        intro-double-negation))

Recent changes