analytic LLPO

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 basic constructions: strong axioms further In real analysis, there is a principle on the Cauchy real numbers which is equivalent in strength to the lesser.