Theorem: max_exp_pos (Ray/Hartogs/MaxLog.lean)

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ 0 < max b.exp x
Tactic:
bound
State after:
no goals