Real numbers from Cauchy sequences #
This file defines ℝ
as the type of equivalence classes of Cauchy sequences of rational numbers.
This choice is motivated by how easy it is to prove that ℝ
is a commutative ring, by simply
lifting everything to ℚ
.
The facts that the real numbers are an Archimedean floor ring,
and a conditionally complete linear order,
have been deferred to the file Mathlib/Data/Real/Archimedean.lean
,
in order to keep the imports here simple.
The fact that the real numbers are a (trivial) *-ring has similarly been deferred to
Mathlib/Data/Real/Star.lean
.
The type ℝ
of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.
- ofCauchy :: (
- cauchy : CauSeq.Completion.Cauchy abs
The underlying Cauchy completion
- )
Instances For
The type ℝ
of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.
Equations
- termℝ = Lean.ParserDescr.node `termℝ 1024 (Lean.ParserDescr.symbol "ℝ")
Instances For
The real numbers are isomorphic to the quotient of Cauchy sequences on the rationals.
Equations
- Real.equivCauchy = { toFun := Real.cauchy, invFun := Real.ofCauchy, left_inv := Real.equivCauchy.proof_1, right_inv := Real.equivCauchy.proof_2 }
Instances For
Equations
- Real.instNatCast = { natCast := fun (n : ℕ) => { cauchy := ↑n } }
Equations
- Real.instIntCast = { intCast := fun (z : ℤ) => { cauchy := ↑z } }
Equations
- Real.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => { cauchy := ↑q } }
Equations
- Real.instRatCast = { ratCast := fun (q : ℚ) => { cauchy := ↑q } }
Real.equivCauchy
as a ring equivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Extra instances to short-circuit type class resolution.
These short-circuits have an additional property of ensuring that a computable path is found; if
Field ℝ
is found first, then decaying it to these typeclasses would result in a noncomputable
version of them.
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
- One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
Show an underlying cauchy sequence for real numbers.
The representative chosen is the one passed in the VM to Quot.mk
, so two cauchy sequences
converging to the same number may be printed differently.
Equations
- Real.instRepr = { reprPrec := fun (r : ℝ) (p : ℕ) => Repr.addAppParen (Std.Format.text "Real.ofCauchy " ++ repr r.cauchy) p }
A ring homomorphism f : α →+* β
is bounded with respect to the functions nα : α → ℝ
and
nβ : β → ℝ
if there exists a positive constant C
such that for all x
in α
,
nβ (f x) ≤ C * nα x
.