Real numbers
Content created by Louis Wasserman, Fredrik Bakke, malarbol and Egbert Rijke.
Created on 2023-04-08.
Last modified on 2025-05-05.
Modules in the real numbers namespace
module real-numbers where open import real-numbers.absolute-value-real-numbers public open import real-numbers.addition-lower-dedekind-real-numbers public open import real-numbers.addition-real-numbers public open import real-numbers.addition-upper-dedekind-real-numbers public open import real-numbers.apartness-real-numbers public open import real-numbers.arithmetically-located-dedekind-cuts public open import real-numbers.cauchy-completeness-dedekind-real-numbers public open import real-numbers.dedekind-real-numbers public open import real-numbers.difference-real-numbers public open import real-numbers.distance-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.isometry-addition-real-numbers public open import real-numbers.isometry-negation-real-numbers public open import real-numbers.lower-dedekind-real-numbers public open import real-numbers.maximum-lower-dedekind-real-numbers public open import real-numbers.maximum-real-numbers public open import real-numbers.maximum-upper-dedekind-real-numbers public open import real-numbers.metric-space-of-real-numbers public open import real-numbers.minimum-lower-dedekind-real-numbers public open import real-numbers.minimum-real-numbers public open import real-numbers.minimum-upper-dedekind-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.nonnegative-real-numbers public open import real-numbers.positive-real-numbers public open import real-numbers.raising-universe-levels-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.transposition-addition-subtraction-cuts-dedekind-real-numbers public open import real-numbers.upper-dedekind-real-numbers public
Recent changes
- 2025-05-05. malarbol. Metric properties of real negation, absolute value, addition and maximum (#1398).
- 2025-04-25. Louis Wasserman. Distance function on real numbers (#1394).
- 2025-04-02. Louis Wasserman. Cauchy completeness of the Dedekind real numbers (#1343).
- 2025-03-27. Louis Wasserman. Addition on real numbers (#1336).
- 2025-03-26. Louis Wasserman and Fredrik Bakke. Absolute value of real numbers (#1385).