twoStepInduction_nil — Mathlib

English

Base case for two-step induction: the motive evaluated at the empty list equals nil.

Русский

Базовый случай двойной индукции: значение мотива на пустом списке равно nil.

LaTeX

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

Lean4

@[simp]
theorem twoStepInduction_nil {motive : (l : List α) → Sort*} (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 [] = nil :=
  twoStepInduction.eq_1 ..

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