Lebesgue’s dominated convergence theorem in Bishop’s style

We present a constructive proof in Bishop’s style of Lebesgue’s dominated convergence theorem in the abstract setting of ordered uniform spaces. The proof generalises to this setting a classical proof in the framework of uniform lattices presented by Hans Weber in [Uniform lattices. II: order continuity and exhaustivity, Annali di Matematica pura ed applicata, (IV) CLXV (1993) 133–158].

► We present a proof of Lebesgue’s dominated convergence theorem.
► The proof is presented in the abstract setting of ordered uniform spaces.
► The proof is done constructively in intuitionistic logic and in Bishop’s style.
► We do not employ any axiom of choice or impredicative construction.
► The proof generalises and makes constructive Weber’s proof for uniform lattices.