tendsto_atBot_isLUB — Mathlib

English

A monotone function with a bounded above range converges to the supremum of its range along atTop.

Русский

Монотонная функция с верхней гранью диапазона сходится к верхней границе диапазона по atTop.

LaTeX

$$$\\text{Monotone } f \\Rightarrow BddAbove (\\mathrm{range}\, f) \\Rightarrow \\text{Tendsto } f\\; atTop\\; (nhds (\\bigvee_i f_i)).$$$

Lean4

theorem tendsto_atBot_isLUB (h_anti : Antitone f) (ha : IsLUB (Set.range f) a) : Tendsto f atBot (𝓝 a) := by
  convert tendsto_atTop_isLUB h_anti.dual_left ha using 1

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