lean_workbook_plus_79533

Proved

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

Express the sequence in terms of two subsequences: $u_{2n-1}=a_n$ and $u_{2n}=b_n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79533 (u : ℕ → ℝ) (a b : ℕ → ℝ) (ha : a = fun (n:ℕ) ↦ u (2 * n - 1)) (hb : b = fun (n:ℕ) ↦ u (2 * n)) : u = fun n ↦ if n % 2 = 0 then b (n / 2) else a ((n + 1) / 2)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph