Theorem: tendsto_atInf_iff_norm_tendsto_atTop (Ray/Misc/AtInf.lean)

State before:
X Y : Type
inst✝ : Norm Y
f : Filter X
g : X → Y
⊢ Tendsto (fun x => g x) f atInf ↔ Tendsto (fun x => ‖g x‖) f atTop
Tactic:
rw [Filter.atTop_basis_Ioi.tendsto_right_iff]
State after:
X Y : Type
inst✝ : Norm Y
f : Filter X
g : X → Y
⊢ Tendsto (fun x => g x) f atInf ↔ ∀ (i : ℝ), True → ∀ᶠ (x : X) in f, ‖g x‖ ∈ Ioi i

State before:
X Y : Type
inst✝ : Norm Y
f : Filter X
g : X → Y
⊢ Tendsto (fun x => g x) f atInf ↔ ∀ (i : ℝ), True → ∀ᶠ (x : X) in f, ‖g x‖ ∈ Ioi i
Tactic:
simp only [atInf_basis.tendsto_right_iff, true_imp_iff, mem_setOf, mem_Ioi]
State after:
no goals