lean_workbook_plus_31771

Proved

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

By the principle of mathematical induction, since $P(1)$ is true and $P(k) \implies P(k+1)$ for all non-negative $k$ , it must be true that $P(n)$ is true for all positive integers $n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_31771  (P : ℕ → Prop)
  (hP : P 1)
  (hP' : ∀ k, P k → P (k + 1)) :
  ∀ n, 0 < n → P n   :=  by sorry

Source

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

View graph