Cantor space

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

Created on 2022-06-30.
Last modified on 2023-03-10.

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

open import foundation.tight-apartness-relations
open import foundation.universe-levels

open import univalent-combinatorics.equality-standard-finite-types
open import univalent-combinatorics.standard-finite-types

Idea

The Cantor space is the type of functions ℕ → Fin 2.

Definition

cantor-space : UU lzero
cantor-space = ℕ → Fin 2

Properties

The cantor space has a tight apartness relation

cantor-space-Type-With-Tight-Apartness : Type-With-Tight-Apartness lzero lzero
cantor-space-Type-With-Tight-Apartness =
  exp-Type-With-Tight-Apartness ℕ (Fin-Type-With-Tight-Apartness 2)

Recent changes