theorem proved tactic proof

`expL_logL`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  98theorem expL_logL {x : LogicReal} (hx : (0 : LogicReal) < x) :
  99    expL (logL x) = x := by

proof body

Tactic-mode proof.

 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. -/

depends on (9)

Lean names referenced from this declaration's body.

expL in IndisputableMonolith.Foundation.LogicRealTranscendentals decl_use
logL in IndisputableMonolith.Foundation.LogicRealTranscendentals decl_use
toReal_expL in IndisputableMonolith.Foundation.LogicRealTranscendentals decl_use
toReal_logL in IndisputableMonolith.Foundation.LogicRealTranscendentals decl_use
eq_iff_toReal_eq in IndisputableMonolith.Foundation.RealsFromLogic decl_use
LogicReal in IndisputableMonolith.Foundation.RealsFromLogic decl_use
lt_iff_toReal_lt in IndisputableMonolith.Foundation.RealsFromLogic decl_use
toReal in IndisputableMonolith.Foundation.RealsFromLogic decl_use
toReal in IndisputableMonolith.Support.RungFractions decl_use