theorem
proved
expL_logL
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.LogicRealTranscendentals on GitHub at line 98.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
102 exact Real.exp_log hx'
103
104/-- Transported logarithm/exponential inverse. -/
105theorem logL_expL (x : LogicReal) : logL (expL x) = x := by
106 rw [eq_iff_toReal_eq, toReal_logL, toReal_expL]
107 exact Real.log_exp _
108
109/-- Transported hyperbolic cosine definition. -/
110theorem coshL_eq_exp (x : LogicReal) :
111 coshL x = (expL x + expL (-x)) / fromReal 2 := by
112 rw [eq_iff_toReal_eq, toReal_coshL, toReal_div, toReal_add, toReal_expL,
113 toReal_expL, toReal_neg, toReal_fromReal]
114 exact Real.cosh_eq _
115
116end
117
118end LogicRealTranscendentals
119end Foundation
120end IndisputableMonolith