tendsto_of_bddBelow_antitone — Mathlib

English

A monotone decreasing sequence bounded below converges to its infimum.

Русский

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

LaTeX

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

Lean4

/-- An antitone, bounded below sequence `f : ℕ → ℝ` has a finite limit. -/
theorem _root_.Real.tendsto_of_bddBelow_antitone {f : ℕ → ℝ} (h_bdd : BddBelow (Set.range f)) (h_ant : Antitone f) :
    ∃ r : ℝ, Tendsto f atTop (𝓝 r) :=
  by
  obtain ⟨B, hB⟩ := Real.exists_isGLB (Set.range_nonempty f) h_bdd
  exact ⟨B, tendsto_atTop_isGLB h_ant hB⟩

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