Real numbers

Content created by Egbert Rijke and malarbol.

Created on 2023-04-08.
Last modified on 2024-02-27.

Files in the real numbers folder

module real-numbers where

open import real-numbers.dedekind-real-numbers public
open import real-numbers.rational-real-numbers public

Recent changes