theorem relaxationSequence_tendsto_inf {α : Type u} [TopologicalSpace α] [ConditionallyCompletePartialOrderInf α] [InfConvergenceClass α] {a : ℕ → α} (ha : ∀ (n : ℕ), a (n + 1) ≤ a n) (hbdd : BddBelow (Set.range a)) : Filter.Tendsto a Filter.atTop (nhds (sInf (Set.range a)))

Proposition 1.4.2: A bounded-below relaxation sequence converges to the infimum of its range.