Cauchy real number

analysis (differential/integral calculus, functional analysis, topology) metric space, normed vector space open ball, open subset, neighbourhood convergence, limit of a sequence compactness, sequential compactness … … constructive mathematics, realizability, computability propositions as types, proofs as programs, computational trinitarianism A Cauchy real number is a real number that is given as the limit of a Cauchy sequence of rational numbers. One may use this idea as a definition of the...