Backwards_Induction

Proved

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

mathematical-inductionnamed-theoremsnumber-theoryproof-techniquesproofwiki

Let $P$ be a propositional function on the natural numbers $\N$ . Suppose that $(1): \quad \forall n \in \N: \map P {2^n}$ holds. $(2): \quad \map P n \implies \map P {n - 1}$ . Then $\map P n$ holds for all $\forall n \in \N$ . The proof technique based on this result is called '''backwards induction'''.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

import Mathlib.Analysis.Complex.Basic

theorem Backwards_Induction (P : ℕ → Prop) (hinf : ∀ n, ∃ m, n ≤ m ∧ P m) (hback : ∀ m, P (m + 1) → P m) : ∀ n, P n := by sorry

Source

https://proofwiki.org/wiki/Backwards_Induction

View graph