cauchy_induction_mul — Mathlib

English

Let P(n) be a property on naturals. If P(n) implies P(n+1) and we have a multiplicative step with k>1, then P(n) holds for all n starting from a base.

Русский

Пусть P(n) — свойство над натуральными. Если P(n) ⇒ P(n+1) и есть умножительный шаг с k>1, то P(n) верно для всех n, начиная с основания.

LaTeX

$$$\\forall P\\,(h:\\nrightarrow P(n+1)\\Rightarrow P(n))\\; (k,seed)\\; (hk:1

Lean4

theorem cauchy_induction_mul (h : ∀ (n : ℕ), P (n + 1) → P n) (k seed : ℕ) (hk : 1 < k) (hs : P seed.succ)
    (hm : ∀ x, seed < x → P x → P (k * x)) (n : ℕ) : P n :=
  by
  apply Nat.cauchy_induction h _ hs (k * ·) fun x hl hP => ⟨_, hm x hl hP⟩
  intro _ hl _
  convert (Nat.mul_lt_mul_right <| seed.succ_pos.trans_le hl).2 hk
  rw [one_mul]

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