α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[Iio a] a) (𝓝 y)
⊢ leftLim f a = y
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
⊢ leftLim f a = y
have h'' : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y) := ⟨y, h'⟩
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[Iio a] a) (𝓝 y)
⊢ leftLim f a = y
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[Iio a] a) (𝓝 y)
⊢ leftLim f a = y
rw [h'α.topology_eq_generate_intervals] at h h' h''
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[Iio a] a) (𝓝 y)
⊢ limUnder (𝓝[Iio a] a) f = y
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[Iio a] a) (𝓝 y)
⊢ leftLim f a = y
simp only [leftLim, h, h'', not_true, or_self_iff, if_false]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[Iio a] a) (𝓝 y)
this : NeBot (𝓝[Iio a] a)
⊢ limUnder (𝓝[Iio a] a) f = y
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[Iio a] a) (𝓝 y)
⊢ limUnder (𝓝[Iio a] a) f = y
haveI := neBot_iff.2 h
no goals
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[Iio a] a) (𝓝 y)
this : NeBot (𝓝[Iio a] a)
⊢ limUnder (𝓝[Iio a] a) f = y
exact lim_eq h'