Theorems · Theorem · general topology

Real.isLUB_of_tendsto_monotone_bddAbove

∀ {ι : Type u_1} [inst : Preorder ι] [Nonempty ι] [IsDirected ι fun x1 x2 => x1 ≤ x2] {f : ι → ℝ} {x : ℝ},
  Filter.Tendsto f Filter.atTop (nhds x) → Monotone f → BddAbove (Set.range f) → IsLUB (Set.range f) x

The limit of a monotone, bounded above function f : ι → ℝ is a least upper bound of the function.

Defined in

Mathlib.Topology.Instances.Real.Lemmas

Cited by

0 results in Mathlib

Foundations

Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderNonemptyIsDirected