Real numbers

Content created by Louis Wasserman, Fredrik Bakke, Egbert Rijke and malarbol.

Created on 2023-04-08.
Last modified on 2025-02-16.

Modules in the real numbers namespace

module real-numbers where

open import real-numbers.apartness-real-numbers public
open import real-numbers.arithmetically-located-dedekind-cuts public
open import real-numbers.dedekind-real-numbers public
open import real-numbers.inequality-lower-dedekind-real-numbers public
open import real-numbers.inequality-real-numbers public
open import real-numbers.inequality-upper-dedekind-real-numbers public
open import real-numbers.lower-dedekind-real-numbers public
open import real-numbers.metric-space-of-real-numbers public
open import real-numbers.negation-lower-upper-dedekind-real-numbers public
open import real-numbers.negation-real-numbers public
open import real-numbers.rational-lower-dedekind-real-numbers public
open import real-numbers.rational-real-numbers public
open import real-numbers.rational-upper-dedekind-real-numbers public
open import real-numbers.similarity-real-numbers public
open import real-numbers.strict-inequality-real-numbers public
open import real-numbers.upper-dedekind-real-numbers public

Recent changes

• 2025-02-16. Louis Wasserman. Break the Dedekind reals into lower and upper Dedekind reals (#1314).
• 2025-02-12. Louis Wasserman and Fredrik Bakke. Apartness for real numbers (#1296).
• 2025-02-08. Louis Wasserman. Similarity of real numbers (#1301).
• 2025-02-08. Fredrik Bakke. Functorial action of existential quantifications, and applications in real-numbers (#1298).
• 2025-02-05. Louis Wasserman. Inequality in ℝ (#1275).