snocInduction — Mathlib

English

Detailed form of snoc induction splitting by Fin.elim0 and Fin.snoc.

Русский

Уточнённая форма индукции по snoc, разделяя Fin.elim0 и Fin.snoc.

LaTeX

$$$\\text{snocInduction}_{\\text{detail}}(h_0,h) := \\text{definition}$$$

Lean4

/-- Recurse on a tuple by splitting into `Fin.elim0` and `Fin.snoc`. -/
@[elab_as_elim]
def snocInduction {α : Sort*} {P : ∀ {n : ℕ}, (Fin n → α) → Sort*} (h0 : P Fin.elim0)
    (h : ∀ {n} (x : Fin n → α) (x₀), P x → P (Fin.snoc x x₀)) : ∀ {n : ℕ} (x : Fin n → α), P x
  | 0, x => by convert h0
  | _ + 1, x => snocCases (fun _ _ ↦ h _ _ <| snocInduction h0 h _) x

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