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)
72noncomputable def toReal (x : LogicReal) : ℝ :=
proof body
Definition body.
73 CompareReals.compareEquiv x.val
74
75/-- Transport a Mathlib real into the recovered real line. -/
used by (40)
From the project-wide theorem graph. These declarations reference this one in their body.
-
PhiInt
in IndisputableMonolith.Algebra.PhiRing
decl_use
-
toComplex
in IndisputableMonolith.Foundation.ComplexFromLogic
decl_use
-
toComplex_im
in IndisputableMonolith.Foundation.ComplexFromLogic
decl_use
-
toComplex_ofLogicReal
in IndisputableMonolith.Foundation.ComplexFromLogic
decl_use
-
toComplex_re
in IndisputableMonolith.Foundation.ComplexFromLogic
decl_use
-
toComplex_re_eq
in IndisputableMonolith.Foundation.LogicComplexCompat
decl_use
-
coshL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
cosL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
expL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
expL_logL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
logL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
rpowL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
sinhL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
sinL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
sqrtL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_coshL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_cosL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_expL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_logL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_piL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_rpowL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_sinhL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_sinL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_sqrtL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
eq_iff_toReal_eq
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
-
equivReal
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
-
fromReal_toReal
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
-
le_iff_toReal_le
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
-
logicReal_recovered_from_completion
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
-
lt_iff_toReal_lt
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
… and 10 more
depends on (2)
Lean names referenced from this declaration's body.
-
LogicReal
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
-
toReal
in IndisputableMonolith.Support.RungFractions
decl_use