case h.e'_5.h
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
l : Filter β
f g : β → α
inst✝ : NoMaxOrder α
a x✝ : α
⊢ Ioo (a - x✝) (a + x✝) = {b | abs (b - a) < x✝}
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
l : Filter β
f g : β → α
inst✝ : NoMaxOrder α
a : α
⊢ HasBasis (𝓝 a) (fun ε => 0 < ε) fun ε => Ioo (a - ε) (a + ε)
convert nhds_basis_abs_sub_lt a
no goals
case h.e'_5.h
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
l : Filter β
f g : β → α
inst✝ : NoMaxOrder α
a x✝ : α
⊢ Ioo (a - x✝) (a + x✝) = {b | abs (b - a) < x✝}
simp only [Ioo, abs_lt, ← sub_lt_iff_lt_add, neg_lt_sub_iff_lt_add, sub_lt_comm]