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

State before:
X Y : Type
inst✝ : Norm Y
f : X → Y
l : Filter X
⊢ Tendsto f l atInf ↔ ∀ (r : ℝ), ∀ᶠ (x : X) in l, r < ‖f x‖
Tactic:
rw [atInf_basis.tendsto_right_iff]
State after:
X Y : Type
inst✝ : Norm Y
f : X → Y
l : Filter X
⊢ (∀ (i : ℝ), True → ∀ᶠ (x : X) in l, f x ∈ {x | i < ‖x‖}) ↔ ∀ (r : ℝ), ∀ᶠ (x : X) in l, r < ‖f x‖

State before:
X Y : Type
inst✝ : Norm Y
f : X → Y
l : Filter X
⊢ (∀ (i : ℝ), True → ∀ᶠ (x : X) in l, f x ∈ {x | i < ‖x‖}) ↔ ∀ (r : ℝ), ∀ᶠ (x : X) in l, r < ‖f x‖
Tactic:
simp only [true_imp_iff, mem_setOf]
State after:
no goals