induction_reflect — Mathlib

English

An induction principle for reflection-based steps of IsPos.

Русский

Индукционное доказательство через отражение IsPos.

LaTeX

$$RootPairing.Base.IsPos.induction_reflect$$

Lean4

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

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