twoStepInduction_singleton — Mathlib

English

Base step of two-step induction for a singleton list [x] yields singleton x.

Русский

Базовый шаг двухшаговой индукции для списка-одиночки [x] даёт singleton x.

LaTeX

$$$$ \operatorname{twoStepInduction} nil singleton cons\_cons [x] = singleton x. $$$$

Lean4

@[simp]
theorem twoStepInduction_singleton {motive : (l : List α) → Sort*} (x : α) (nil : motive [])
    (singleton : ∀ x, motive [x]) (cons_cons : ∀ x y xs, motive xs → (∀ y, motive (y :: xs)) → motive (x :: y :: xs)) :
    twoStepInduction nil singleton cons_cons [x] = singleton x :=
  twoStepInduction.eq_2 ..

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