English
The left limit of a function f at a, denoted leftLim f a, is defined by the order topology on α: it equals the left-hand limit limUnder (nhds[<] a) f when this limit exists and nhds[<] a ≠ ⊥; otherwise it is defined to be f a.
Русский
Левая граница функции f в точке a определяется по топологии порядка на α: она равна левой границе limUnder (nhds[<] a) f, если предел существует и nhds[<] a не равно ⊥; в противном случае задаётся f(a).
LaTeX
$$$\operatorname{leftLim}(f,a) = \begin{cases} \lim_{\mathcal{N}_{<}(a)} f & \text{если } 𝓝[<] a \neq ⊥ \text{ и существует предел}, \\ f(a) & \text{иначе}. \end{cases}$$$
Lean4
/-- Let `f : α → β` be a function from a linear order `α` to a topological space `β`, and
let `a : α`. The limit strictly to the left of `f` at `a`, denoted with `leftLim f a`, is defined
by using the order topology on `α`. If `a` is isolated to its left or the function has no left
limit, we use `f a` instead to guarantee a good behavior in most cases. -/
noncomputable def leftLim (f : α → β) (a : α) : β := by
classical
haveI : Nonempty β := ⟨f a⟩
letI : TopologicalSpace α := Preorder.topology α
exact if 𝓝[<] a = ⊥ ∨ ¬∃ y, Tendsto f (𝓝[<] a) (𝓝 y) then f a else limUnder (𝓝[<] a) f
