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
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).
- 2023-03-06. Fredrik Bakke. Remove redundant whitespace in headers (#486).