induction_add — Mathlib

English

An induction principle that uses addition of roots to step through positive heights.

Русский

Индукция по сумме корней через сложение корней.

LaTeX

$$RootPairing.Base.IsPos.induction_add$$

Lean4

theorem induction_add (i : ι) {p : ι → Prop} (h₀ : ∀ i, p i → p (P.reflectionPerm i i)) (h₁ : ∀ i ∈ b.support, p i)
    (h₂ : ∀ i j k, P.root k = P.root i + P.root j → p i → j ∈ b.support → p k) : p i :=
  by
  letI := P.indexNeg
  rcases IsPos.or_neg b i with hi | hi
  · exact hi.induction_on_add h₁ h₂
  · suffices p (-i) by rw [← neg_neg i]; exact h₀ (-i) this
    exact hi.induction_on_add h₁ h₂

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