theorem Sequences.monotone_increasing_iff (x : ℕ → ℝ) : Monotone x ↔ ∀ (n : ℕ), x n ≤ x (n + 1)

A sequence x : ℕ → ℝ is monotone increasing (i.e. Monotone x) if and only if each term is bounded above by its immediate successor: x n ≤ x (n + 1) for all n.

theorem Sequences.monotone_decreasing_convergence (x : ℕ → ℝ) (hm : Antitone x) : ((∃ (L : ℝ), Filter.Tendsto x Filter.atTop (nhds L)) ↔ BddBelow (Set.range x)) ∧ (BddBelow (Set.range x) → Filter.Tendsto x Filter.atTop (nhds (⨅ (n : ℕ), x n)))

A monotone decreasing real sequence converges if and only if it is bounded below, and in that case its limit equals the infimum of its range: a monotone decreasing sequence x converges iff BddBelow (Set.range x), and when bounded below, the sequence converges to ⨅ n, x n.