English
Let α be a type. For any n, element x ∈ α and vector v ∈ Vector α n, and any predicate C on vectors, with base case nil : C nil and step cons : ∀ {n} {x : α} {w : Vector α n}, C w → C (x ::ᵥ w), we have (x ::ᵥ v).inductionOn nil cons = cons (v.inductionOn nil cons).
Русский
Пусть α — тип. Для любого n, элемента x ∈ α и вектора v ∈ Vector α n, и любого предиката C на вектора, имеем базовый случай nil : C nil и переход cons : ∀ {n} {x : α} {w : Vector α n}, C w → C (x ::ᵥ w). Тогда (x ::ᵥ v).inductionOn nil cons = cons (v.inductionOn nil cons).
LaTeX
$$$ (x \\;::^\\vee\\; v).inductionOn\\; nil\\; cons = cons\\big( v.inductionOn\\; nil\\; cons \\big) $$$
Lean4
@[simp]
theorem inductionOn_cons {C : ∀ {n : ℕ}, Vector α n → Sort*} {n : ℕ} (x : α) (v : Vector α n) (nil : C nil)
(cons : ∀ {n : ℕ} {x : α} {w : Vector α n}, C w → C (x ::ᵥ w)) :
(x ::ᵥ v).inductionOn nil cons = cons (v.inductionOn nil cons : C v) :=
rfl
