no goals
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
a ε : α
hε : 0 < ε
⊢ {x | (fun x => abs (x - a) < ε) x} ∈ 𝓟 {b | abs (a - b) < ε}
simp only [abs_sub_comm, mem_principal_self]