Cantor space

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Louis Wasserman.

Created on 2022-06-30.
Last modified on 2025-10-25.

module set-theory.cantor-space where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.booleans
open import foundation.dependent-pair-types
open import foundation.double-negation-stable-equality
open import foundation.function-types-with-apartness-relations
open import foundation.sets
open import foundation.tight-apartness-relations
open import foundation.universe-levels

open import set-theory.cantors-diagonal-argument
open import set-theory.uncountable-sets

Idea

The Cantor space is the set of functions ℕ → bool. In other words, it is the set of binary sequences.

Definition

cantor-space : UU lzero
cantor-space = ℕ → bool

Properties

The cantor space has a tight apartness relation

tight-apartness-relation-cantor-space :
  Tight-Apartness-Relation lzero cantor-space
tight-apartness-relation-cantor-space =
  tight-apartness-relation-function-into-Type-With-Tight-Apartness
    ( ℕ)
    ( bool-Type-With-Tight-Apartness)

cantor-space-Type-With-Tight-Apartness :
  Type-With-Tight-Apartness lzero lzero
cantor-space-Type-With-Tight-Apartness =
  function-into-Type-With-Tight-Apartness
    ( ℕ)
    ( bool-Type-With-Tight-Apartness)

The cantor space has double negation stable equality

has-double-negation-stable-equality-cantor-space :
  has-double-negation-stable-equality cantor-space
has-double-negation-stable-equality-cantor-space =
  has-double-negation-stable-equality-type-Type-With-Tight-Apartness
    cantor-space-Type-With-Tight-Apartness

The cantor space is a set

is-set-cantor-space : is-set cantor-space
is-set-cantor-space = is-set-function-type is-set-bool

cantor-space-Set : Set lzero
cantor-space-Set = (cantor-space , is-set-cantor-space)

The cantor space is uncountable

is-uncountable-cantor-space : is-uncountable cantor-space-Set
is-uncountable-cantor-space =
  is-uncountable-sequence-discrete-type-diagonal-argument-Cantor
    ( bool-Discrete-Type)
    ( true)
    ( false)
    ( neq-true-false-bool)

Recent changes