lean_workbook_plus_68616

Proved

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

How many sequences of natural number such that $1 \le {a_1}<{a_2} <.....<{a_k}\le n$ and ${a_i} \equiv {i} \pmod {2} \forall i$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68616 (n k : ℕ) : n ≥ k → ∃ a : ℕ → ℕ, (∀ i : ℕ, 1 ≤ i ∧ i ≤ k → a i ≡ i [ZMOD 2] ∧ a i < a (i + 1)) ∧ a k ≤ n   :=  by sorry

Source

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

View graph