pith. machine review for the scientific record. sign in
theorem proved term proof

toReal_ofRatCore

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 113theorem toReal_ofRatCore (q : ℚ) : toReal (ofRatCore q) = (q : ℝ) := by

proof body

Term-mode proof.

 114  -- `CompareReals.compareEquiv` is the unique completion comparison map;
 115  -- on dense rational points it agrees with the usual rational coercion.
 116  simpa [toReal, ofRatCore, CompareReals.compareEquiv] using
 117    (CompareReals.bourbakiPkg.compare_coe rationalCauSeqPkg
 118      (show CompareReals.Q from q))
 119

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.