Module mathcomp.reals.reals

# An axiomatization of real numbers $\mathbb{R}$ This file provides a classical axiomatization of real numbers as a discrete real archimedean field with in particular a theory of floor and ceil. ``` realType == type of real numbers The HB class is Real. sup A == where A : set R with R : realType, the supremum of A when it exists, 0 otherwise inf A := - sup (- A) ``` The mixin corresponding to realType extends an archiFieldType with two properties: - when sup A exists, it is an upper bound of A (lemma sup_upper_bound) - when sup A exists, there exists an element x in A such that sup A - eps < x for any 0 < eps (lemma sup_adherent) ``` Rint == the set of real numbers that can be written as z%:~R, i.e., as an integer Rtoint r == r when r is an integer, 0 otherwise floor_set x := [set y | Rtoint y /\ y <= x] Rfloor x == the floor of x as a real number range1 x := [set y |x <= y < x + 1] Rceil x == the ceil of x as a real number, i.e., - Rfloor (- x) ``` ``` @rational R == set of rational numbers of type R : realType @irrational R == the complement of rational R ```