def
definition
expL
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.LogicRealTranscendentals on GitHub at line 29.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
26def sqrtL (x : LogicReal) : LogicReal := fromReal (Real.sqrt (toReal x))
27
28/-- Exponential on recovered reals, transported from `Real.exp`. -/
29def expL (x : LogicReal) : LogicReal := fromReal (Real.exp (toReal x))
30
31/-- Natural logarithm on recovered reals, transported from `Real.log`. -/
32def logL (x : LogicReal) : LogicReal := fromReal (Real.log (toReal x))
33
34/-- Real power on recovered reals, transported from `Real.rpow`. -/
35def rpowL (x y : LogicReal) : LogicReal := fromReal (Real.rpow (toReal x) (toReal y))
36
37/-- The recovered constant π. -/
38def piL : LogicReal := fromReal Real.pi
39
40/-- Sine on recovered reals. -/
41def sinL (x : LogicReal) : LogicReal := fromReal (Real.sin (toReal x))
42
43/-- Cosine on recovered reals. -/
44def cosL (x : LogicReal) : LogicReal := fromReal (Real.cos (toReal x))
45
46/-- Hyperbolic sine on recovered reals. -/
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