Loeb, Iris Lipschitz functions in constructive reverse mathematics. (English) Zbl 1277.03062 Log. J. IGPL 21, No. 1, 28-43 (2013). In this paper, different formulations of Lipschitz continuity (of functions with compact domain) are studied from the perspective of constructive reverse mathematics.Recall that in constructive mathematics the usual definition of continuous functions on a compact domain automatically assume uniform continuity. (This goes back to Bishop.)This paper belongs to a series of papers where one breaks with this custom and studies functions that are defined to be, a priori, pointwise continuous and what logical principles are needed to get uniform continuity; see [H. Diener and the author, J. Log. Anal. 3, Article 8, 26 p. (2011; Zbl 1291.03115)] for previous work.Here, in particular, the property of Lipschitz continuity is studied. There are statements that a locally Lipschitz continuous function \(f\) is uniformly Lipschitz for(1) \(f: 2^\mathbb{N} \to \mathbb{R}\), (2) \(f: [0,1] \to \mathbb{R}\) and with a continuous modulus of Lipschitz continuity, (3) \(f: 2^\mathbb{N} \to \mathbb{N}\). It is show that the case (1) follows from the fan theorem for \(\Pi^0_1\)-bars, the case (2) follows from the uniform continuity theorem and with this also from this fan theorem, and (3) follows from the fan theorem for continuous bars. Reviewer: Alexander Kreuzer (Lyon) Cited in 2 Documents MSC: 03F60 Constructive and recursive analysis 03B30 Foundations of classical theories (including reverse mathematics) 26A16 Lipschitz (Hölder) classes Keywords:constructive reverse mathematics; Lipschitz continuity; fan theorem; constructive mathematics Citations:Zbl 1291.03115 PDFBibTeX XMLCite \textit{I. Loeb}, Log. J. IGPL 21, No. 1, 28--43 (2013; Zbl 1277.03062) Full Text: DOI