rightLim_eq_of_tendsto — Mathlib

English

If nhds[>] a ≠ ⊥ and f tends to y along nhds[>] a, then rightLim f a = y.

Русский

Если правая окрестность nhds[>] a не пуста и f стремится к y вдоль nhds[>] a, то rightLim f a = y.

LaTeX

$$$\text{If } 𝓝[>] a \neq ⊥ \text{ and } \operatorname{Tendsto}(f, 𝓝[>] a, 𝓝 y), \text{ then } \operatorname{rightLim}(f,a) = y$$$

Lean4

theorem rightLim_eq_of_tendsto [TopologicalSpace α] [OrderTopology α] [T2Space β] {f : α → β} {a : α} {y : β}
    (h : 𝓝[>] a ≠ ⊥) (h' : Tendsto f (𝓝[>] a) (𝓝 y)) : Function.rightLim f a = y :=
  @leftLim_eq_of_tendsto αᵒᵈ _ _ _ _ _ _ f a y h h'

Похожие утверждения