no goals
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
x : Filter β
a : α
⊢ Tendsto f x (𝓝 a) ↔ ∀ (ε : α), ε > 0 → ∀ᶠ (b : β) in x, abs (f b - a) < ε
simp [nhds_eq_iInf_abs_sub, abs_sub_comm a]