theorem
proved
toReal_logL
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.LogicRealTranscendentals on GitHub at line 60.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
57 toReal (expL x) = Real.exp (toReal x) :=
58 toReal_fromReal _
59
60@[simp] theorem toReal_logL (x : LogicReal) :
61 toReal (logL x) = Real.log (toReal x) :=
62 toReal_fromReal _
63
64@[simp] theorem toReal_rpowL (x y : LogicReal) :
65 toReal (rpowL x y) = Real.rpow (toReal x) (toReal y) :=
66 toReal_fromReal _
67
68@[simp] theorem toReal_piL : toReal piL = Real.pi :=
69 toReal_fromReal _
70
71@[simp] theorem toReal_sinL (x : LogicReal) :
72 toReal (sinL x) = Real.sin (toReal x) :=
73 toReal_fromReal _
74
75@[simp] theorem toReal_cosL (x : LogicReal) :
76 toReal (cosL x) = Real.cos (toReal x) :=
77 toReal_fromReal _
78
79@[simp] theorem toReal_sinhL (x : LogicReal) :
80 toReal (sinhL x) = Real.sinh (toReal x) :=
81 toReal_fromReal _
82
83@[simp] theorem toReal_coshL (x : LogicReal) :
84 toReal (coshL x) = Real.cosh (toReal x) :=
85 toReal_fromReal _
86
87/-- Transported positivity of exponential. -/
88theorem expL_pos (x : LogicReal) : (0 : LogicReal) < expL x := by
89 rw [lt_iff_toReal_lt, toReal_zero, toReal_expL]
90 exact Real.exp_pos _