theorem
proved
toReal_sinL
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.LogicRealTranscendentals on GitHub at line 71.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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 _
91
92/-- Transported non-negativity of square root. -/
93theorem sqrtL_nonneg (x : LogicReal) : (0 : LogicReal) ≤ sqrtL x := by
94 rw [le_iff_toReal_le, toReal_zero, toReal_sqrtL]
95 exact Real.sqrt_nonneg _
96
97/-- Transported exponential/log inverse on positive recovered reals. -/
98theorem expL_logL {x : LogicReal} (hx : (0 : LogicReal) < x) :
99 expL (logL x) = x := by
100 rw [eq_iff_toReal_eq, toReal_expL, toReal_logL]
101 have hx' : 0 < toReal x := by simpa [lt_iff_toReal_lt] using hx