𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
hpq : q < p
⊢ Tendsto (fun x => x ^ (↑p - ↑q)) atTop atTop
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
hpq : q < p
⊢ Tendsto (fun x => x ^ p / x ^ q) atTop atTop
rw [tendsto_congr' pow_div_pow_eventuallyEq_atTop]
case hn
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
hpq : q < p
⊢ 0 < ↑p - ↑q
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
hpq : q < p
⊢ Tendsto (fun x => x ^ (↑p - ↑q)) atTop atTop
apply tendsto_zpow_atTop_atTop
no goals
case hn
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
hpq : q < p
⊢ 0 < ↑p - ↑q
linarith