English
The right limit of f at a is defined by applying the left limit to the dual order αᵒᵈ: rightLim f a = leftLim with respect to the reversed order.
Русский
Правая граница функции f в точке a задаётся как левая граница функции f в порядке, обращённом дуально, то есть по отношению к αᵒᵈ.
LaTeX
$$$\operatorname{rightLim}(f,a) = \operatorname{leftLim}(f,a)\text{ in the order dual } α^{op}$$$
Lean4
/-- Let `f : α → β` be a function from a linear order `α` to a topological space `β`, and
let `a : α`. The limit strictly to the right of `f` at `a`, denoted with `rightLim f a`, is defined
by using the order topology on `α`. If `a` is isolated to its right or the function has no right
limit, we use `f a` instead to guarantee a good behavior in most cases. -/
noncomputable def rightLim (f : α → β) (a : α) : β :=
@Function.leftLim αᵒᵈ β _ _ f a
