lean_workbook_plus_40308

Proved

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

For all,n : (if n is odd ,then $a_n = 0$ ) and ( if n is even,then $a_n =\frac{n}{2}$ ).\nNow let us see if logic allows for that definition.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_40308 (n : ℕ) (a : ℕ → ℕ) (h₁ : ∀ n, Odd n → a n = 0) (h₂ : ∀ n, Even n → a n = n / 2) : (∀ n, (Odd n ∨ Even n) → a n = 0 ∨ a n = n / 2)   :=  by sorry

Source

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

View graph