English
If nhds[<] a ≠ ⊥ and f tends to y along nhds[<] a, then leftLim f a = y.
Русский
Если nhds[<] a не равно ⊥ и функция стремится к y вдоль nhds[<] a, то leftLim f a = y.
LaTeX
$$$\text{If } 𝓝[<] a \neq ⊥ \text{ and } \operatorname{Tendsto}(f, 𝓝[<] a, 𝓝 y), \text{ then } \operatorname{leftLim}(f,a) = y$$$
Lean4
theorem leftLim_eq_of_tendsto [hα : TopologicalSpace α] [h'α : OrderTopology α] [T2Space β] {f : α → β} {a : α} {y : β}
(h : 𝓝[<] a ≠ ⊥) (h' : Tendsto f (𝓝[<] a) (𝓝 y)) : leftLim f a = y :=
by
have h'' : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y) := ⟨y, h'⟩
rw [h'α.topology_eq_generate_intervals] at h h' h''
simp only [leftLim, h, h'', not_true, or_self_iff, if_false]
haveI := neBot_iff.2 h
exact lim_eq h'
