Real numbers

Content created by Egbert Rijke, Fredrik Bakke and malarbol.

Created on 2023-04-08.
Last modified on 2024-09-28.

Modules in the real numbers namespace

module real-numbers where

open import real-numbers.dedekind-real-numbers public
open import real-numbers.metric-space-of-real-numbers public
open import real-numbers.rational-real-numbers public

Recent changes

• 2024-09-28. malarbol and Fredrik Bakke. Metric spaces (#1162).
• 2024-09-23. Fredrik Bakke. Some typos, wording improvements, and brief prose additions (#1186).
• 2024-02-27. malarbol. Rational real numbers (#1034).
• 2023-05-06. Egbert Rijke. Collecting some easily defined precategories (#598).
• 2023-04-08. Egbert Rijke. Refactoring elementary number theory files (#546).