def
definition
coshL
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.LogicRealTranscendentals on GitHub at line 50.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
47def sinhL (x : LogicReal) : LogicReal := fromReal (Real.sinh (toReal x))
48
49/-- Hyperbolic cosine on recovered reals. -/
50def coshL (x : LogicReal) : LogicReal := fromReal (Real.cosh (toReal x))
51
52@[simp] theorem toReal_sqrtL (x : LogicReal) :
53 toReal (sqrtL x) = Real.sqrt (toReal x) :=
54 toReal_fromReal _
55
56@[simp] theorem toReal_expL (x : LogicReal) :
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) :=