Real numbers
InstanceOrder#
Mathlib states this as Real.linearOrder.
Real.linearOrder : LinearOrder ℝ
Sources
Sources
Uses 1 · Used by 44
Statement usesReal number
Used byThe Irrationality of the Square Root of 2 · The Ballot Problem · Sum of a Geometric Series · Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof) · Divergence of the Prime Reciprocal Series · The Triangle Inequality · Stieltjes measure · Absolutely convergent series in Banach spaces · Completeness of spaces of bounded continuous functions · Norm of a continuous linear map · Topology on a normed vector space · Ruzsa covering lemma · Small tripling implies small powers · Triangle counting lemma · Translation number · Euclidean affine space · Geometric law · Urysohn's lemma · Arzela-Ascoli theorem · Baire theorem · Ball · Metric space · Haar measure on a locally compact Hausdorff group · Uniformly continuous function · Bolzano–Weierstrass theorem (1000+ theorems) · Lebesgue differentiation theorem · Bounded convergence theorem · Hahn decomposition theorem · Vitali covering theorem · M. Riesz extension theorem · Krein–Milman theorem · Beatty's theorem · Ostrowski's theorem · Slutsky's theorem · Sylvester's law of inertia (existence) · Complex exponential · Alternating series · Convergence of \(p\)-series for \(p>1\) · Weierstrass polynomial approximation theorem · Bolzano-Weierstrass theorem (Topology of R) · Completeness of R · Complete metric spaces · Limits of sequences · Path connectedness
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.