tendsto_nhdsGT — Mathlib

English

For an antitone function on Ioi x, the right-limit is sInf of its image (bounded below).

Русский

Для антитонной функции на Ioi x правый предел равен sInf образа, если он ограничен снизу.

LaTeX

$$$\mathrm{AntitoneOn}(f, Ioi(x)) \Rightarrow \mathrm{Tendsto}\, f\,(\mathcal{N}_{[>]}(x))\,(\mathcal{N}(\mathrm{sInf}(f'' Ioi(x))))$$$

Lean4

theorem tendsto_nhdsGT {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
    [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α}
    (Af : AntitoneOn f (Ioi x)) (h_bdd : BddAbove (f '' Ioi x)) : Tendsto f (𝓝[>] x) (𝓝 (sSup (f '' Ioi x))) :=
  MonotoneOn.tendsto_nhdsGT Af.dual_right h_bdd

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