cauchy_induction_two_mul — Mathlib

English

Let P be a property on naturals. If P(n) implies P(n+1) and starting from seed, P is closed under doubling, then P holds for all n.

Русский

Пусть P — свойство над натуральными. Если P(n) ⇒ P(n+1) и основание, а затем для всех n, P(n) ⇒ P(2n), то P верно для всех n.

LaTeX

$$$\\text{Nat}.cauchy_induction_mul(h,\\, \\text{seed})$$$

Lean4

theorem cauchy_induction_two_mul (h : ∀ n, P (n + 1) → P n) (seed : ℕ) (hs : P seed.succ)
    (hm : ∀ x, seed < x → P x → P (2 * x)) (n : ℕ) : P n :=
  Nat.cauchy_induction_mul h 2 seed Nat.one_lt_two hs hm n

Похожие утверждения