English
An induction principle for Chebyshev polynomials on integers: to prove a property for all integers, it suffices to verify it at 0 and 1, and show how to propagate by +1 and -1 steps.
Русский
Принцип индукции для Чебышёвых полиномиальных функций на целых: чтобы доказать свойство для всех целых, достаточно доказать для 0 и 1 и показать переходы на +1 и -1.
LaTeX
$$@ Theorem Chebyshev.induct: ∀ (motive: ℤ → Prop), motive 0 → motive 1 → (∀ n, motive (n+1) → motive n → motive (n+2)) → (∀ n, motive (-n) → motive (-n+1) → motive (-n-1)) → ∀ a, motive a$$
Lean4
/-- Induction principle used for proving facts about Chebyshev polynomials. -/
@[elab_as_elim]
protected theorem induct (motive : ℤ → Prop) (zero : motive 0) (one : motive 1)
(add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2))
(neg_add_one : ∀ (n : ℕ), motive (-↑n) → motive (-↑n + 1) → motive (-↑n - 1)) : ∀ (a : ℤ), motive a :=
T.induct motive zero one add_two fun n hn hnm => by simpa only [Int.negSucc_eq, neg_add] using neg_add_one n hn hnm
