Theorem: ENNReal_rpow_lt_top (ForML/SchwartzLp.lean)

State before:
a : ENNReal
p : ℝ
hp : 0 < p
h : a < ⊤
⊢ a ^ p < ⊤
Tactic:
rw [lt_top_iff_ne_top] at h ⊢
State after:
a : ENNReal
p : ℝ
hp : 0 < p
h : a ≠ ⊤
⊢ a ^ p ≠ ⊤

State before:
a : ENNReal
p : ℝ
hp : 0 < p
h : a ≠ ⊤
⊢ a ^ p ≠ ⊤
Tactic:
exact ENNReal_rpow_ne_top hp h
State after:
no goals