iSup_eq_of_tendsto — Mathlib

English

If a monotone f: β → α tends to a along atTop, then iSup f equals a.

Русский

Если монотонная функция f достигает предела a при atTop, тогда iSup f = a.

LaTeX

$$$ \operatorname{Tendsto} f \operatorname{atTop} (\nhds a) \Rightarrow \mathrm{iSup} f = a $$$

Lean4

theorem iSup_eq_of_tendsto {α β} [TopologicalSpace α] [CompleteLinearOrder α] [OrderTopology α] [Nonempty β]
    [SemilatticeSup β] {f : β → α} {a : α} (hf : Monotone f) : Tendsto f atTop (𝓝 a) → iSup f = a :=
  tendsto_nhds_unique (tendsto_atTop_iSup hf)

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