rightLim_eq_of_eq_bot — Mathlib

English

If nhds[>] a = ⊥, then rightLim f a = f a.

Русский

Если правая окрестность nhds[>] a тождественно пустая, то правая граница равна значению в точке: rightLim f a = f a.

LaTeX

$$$\nhds[>] a = ⊥ \Rightarrow \operatorname{rightLim}(f,a) = f(a)$$$

Lean4

theorem rightLim_eq_of_eq_bot [TopologicalSpace α] [OrderTopology α] (f : α → β) {a : α} (h : 𝓝[>] a = ⊥) :
    rightLim f a = f a :=
  @leftLim_eq_of_eq_bot αᵒᵈ _ _ _ _ _ f a h

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