def
definition
piL
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.LogicRealTranscendentals on GitHub at line 38.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
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 :=