Real numbers

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

Created on 2023-04-08.
Last modified on 2025-10-25.

Modules in the real numbers namespace

module real-numbers where

open import real-numbers.absolute-value-closed-intervals-real-numbers public
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.binary-maximum-real-numbers public
open import real-numbers.binary-minimum-real-numbers public
open import real-numbers.cauchy-completeness-dedekind-real-numbers public
open import real-numbers.cauchy-sequences-real-numbers public
open import real-numbers.closed-intervals-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.enclosing-closed-rational-intervals-real-numbers public
open import real-numbers.finitely-enumerable-subsets-real-numbers public
open import real-numbers.inequality-lower-dedekind-real-numbers public
open import real-numbers.inequality-positive-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.infima-and-suprema-families-real-numbers public
open import real-numbers.infima-families-real-numbers public
open import real-numbers.inhabited-finitely-enumerable-subsets-real-numbers public
open import real-numbers.inhabited-totally-bounded-subsets-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.limits-sequences-real-numbers public
open import real-numbers.lipschitz-continuity-multiplication-real-numbers public
open import real-numbers.lower-dedekind-real-numbers public
open import real-numbers.maximum-finite-families-real-numbers public
open import real-numbers.maximum-inhabited-finitely-enumerable-subsets-real-numbers public
open import real-numbers.maximum-lower-dedekind-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-finite-families-real-numbers public
open import real-numbers.minimum-inhabited-finitely-enumerable-subsets-real-numbers public
open import real-numbers.minimum-lower-dedekind-real-numbers public
open import real-numbers.minimum-upper-dedekind-real-numbers public
open import real-numbers.multiplication-negative-real-numbers public
open import real-numbers.multiplication-nonnegative-real-numbers public
open import real-numbers.multiplication-positive-real-numbers public
open import real-numbers.multiplication-real-numbers public
open import real-numbers.multiplicative-inverses-negative-real-numbers public
open import real-numbers.multiplicative-inverses-nonzero-real-numbers public
open import real-numbers.multiplicative-inverses-positive-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.negative-real-numbers public
open import real-numbers.nonnegative-real-numbers public
open import real-numbers.nonzero-real-numbers public
open import real-numbers.positive-and-negative-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.real-numbers-from-lower-dedekind-real-numbers public
open import real-numbers.real-numbers-from-upper-dedekind-real-numbers public
open import real-numbers.saturation-inequality-real-numbers public
open import real-numbers.similarity-real-numbers public
open import real-numbers.square-roots-nonnegative-real-numbers public
open import real-numbers.squares-real-numbers public
open import real-numbers.strict-inequality-nonnegative-real-numbers public
open import real-numbers.strict-inequality-positive-real-numbers public
open import real-numbers.strict-inequality-real-numbers public
open import real-numbers.subsets-real-numbers public
open import real-numbers.suprema-families-real-numbers public
open import real-numbers.totally-bounded-subsets-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