isLUB_of_tendsto_atTop — Mathlib

English

If f is monotone and f tends to a along atTop, then a is the least upper bound of the range of f.

Русский

Если f монотонна и стремится к a по atTop, то a является наименьшей верхней границей образа f.

LaTeX

$$$ \text{Monotone}(f) \wedge \operatorname{Tendsto} f \operatorname{atTop} (\nhds a) \Rightarrow IsLUB(\operatorname{range} f, a) $$$

Lean4

theorem isLUB_of_tendsto_atTop [TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [Nonempty β] [SemilatticeSup β]
    {f : β → α} {a : α} (hf : Monotone f) (ha : Tendsto f atTop (𝓝 a)) : IsLUB (Set.range f) a :=
  by
  constructor
  · rintro _ ⟨b, rfl⟩
    exact hf.ge_of_tendsto ha b
  · exact fun _ hb => le_of_tendsto' ha fun x => hb (Set.mem_range_self x)

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