Theorems · Theorem · combinatorics

List.Vector.inductionOn_cons

∀ {α : Type u_1} {C : {n : ℕ} → List.Vector α n → Sort u_6} {n : ℕ} (x : α) (v : List.Vector α n)
  (nil : C List.Vector.nil) (cons : {n : ℕ} → {x : α} → {w : List.Vector α n} → C w → C (x ::ᵥ w)),
  ((x ::ᵥ v).inductionOn nil fun {n} {x} {w} => cons) = cons (v.inductionOn nil fun {n} {x} {w} => cons)

Defined in

Mathlib.Data.Vector.Basic

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext