no goals
α : Type u_2
β : Type u_1
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
h_mono : Monotone f
h_dense : DenseRange f
a : α
⊢ closure (f '' univ) ∈ 𝓝 (f a)
simp only [image_univ, h_dense.closure_eq, univ_mem]