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)
76noncomputable def fromReal (x : ℝ) : LogicReal :=
proof body
Definition body.
77 ⟨CompareReals.compareEquiv.symm x⟩
78
used by (17)
From the project-wide theorem graph. These declarations reference this one in their body.
-
fromComplex
in IndisputableMonolith.Foundation.ComplexFromLogic
decl_use
-
coshL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
coshL_eq_exp
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
cosL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
expL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
logL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
piL
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
-
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
-
logicReal_recovered_from_completion
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
-
toReal_fromReal
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
-
toReal_ofLogicRat
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
depends on (1)
Lean names referenced from this declaration's body.
-
LogicReal
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use