lean_workbook_plus_674

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Find the limit point of the sequence $u_n= \left\{ \begin{array}{ll} n & \text{if n is odd} \ \frac{1}{n} &\text{if n is even} \end{array} \right.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_674 (u : ℕ → ℝ) (h : ∀ n, if n % 2 = 0 then u n = 1 / n else u n = n) : 0 ∈ closure (Set.range u)   :=  by sorry

Source