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)
66structure LogicReal where
67 val : CompareReals.Bourbakiℝ
68
69namespace LogicReal
70
71/-- Transport a recovered real to Mathlib's real line. -/
used by (40)
From the project-wide theorem graph. These declarations reference this one in their body.
-
LogicComplex
in IndisputableMonolith.Foundation.ComplexFromLogic
decl_use
-
ofLogicRat
in IndisputableMonolith.Foundation.ComplexFromLogic
decl_use
-
ofLogicReal
in IndisputableMonolith.Foundation.ComplexFromLogic
decl_use
-
toComplex_ofLogicReal
in IndisputableMonolith.Foundation.ComplexFromLogic
decl_use
-
real_supports_logic
in IndisputableMonolith.Foundation.DomainBootstrap
decl_use
-
toComplex_re_eq
in IndisputableMonolith.Foundation.LogicComplexCompat
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
-
expL_logL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
expL_pos
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
logL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
logL_expL
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
-
sqrtL_nonneg
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_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
-
add_assoc'
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
-
add_comm'
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
… and 10 more