α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : 𝓝[Iio a] a = ⊥
⊢ leftLim f a = f a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : 𝓝[Iio a] a = ⊥
⊢ leftLim f a = f a
rw [h'α.topology_eq_generate_intervals] at h
no goals
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : 𝓝[Iio a] a = ⊥
⊢ leftLim f a = f a
simp [leftLim, ite_eq_left_iff, h]