inductionOn_nil — Mathlib

English

The induction principle for a vector specialized to nil yields nil when applied to the nil case.

Русский

Специализация принципа индукции на пустой вектор даёт nil в базовом случае.

LaTeX

$$$\\mathrm{inductionOn\\_nil} \\; (nil) \\; (\\mathrm cons) = nil$$$

Lean4

@[simp]
theorem inductionOn_nil {C : ∀ {n : ℕ}, Vector α n → Sort*} (nil : C nil)
    (cons : ∀ {n : ℕ} {x : α} {w : Vector α n}, C w → C (x ::ᵥ w)) : Vector.nil.inductionOn nil cons = nil :=
  rfl

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