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

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ b ≤ maxLog b x
Tactic:
rw [maxLog, Real.le_log_iff_exp_le max_exp_pos]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ b.exp ≤ max b.exp x

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