tendsto_of_bddAbove_monotone — Mathlib

English

A monotone sequence that is bounded above converges to a real limit; its limit is the supremum of its range.

Русский

Убывающая/возрастающая последовательность, ограниченная сверху, сходится к пределе в ℝ и предел равен верхней границе множества значений.

LaTeX

$$∃ r ∈ ℝ, Tendsto f atTop (nhds r) and r = sup range f$$

Lean4

/-- A monotone, bounded above sequence `f : ℕ → ℝ` has a finite limit. -/
theorem _root_.Real.tendsto_of_bddAbove_monotone {f : ℕ → ℝ} (h_bdd : BddAbove (Set.range f)) (h_mon : Monotone f) :
    ∃ r : ℝ, Tendsto f atTop (𝓝 r) :=
  by
  obtain ⟨B, hB⟩ := Real.exists_isLUB (Set.range_nonempty f) h_bdd
  exact ⟨B, tendsto_atTop_isLUB h_mon hB⟩

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