init_def — Mathlib

English

Initialization commutes with taking a family q: Fin(n+1) → α, giving init (λ k, q k) = λ k, q k.castSucc.

Русский

Инициализация коммутирует взятие функции семейства q: Fin(n+1) → α: init (λ k, q k) = λ k, q k.castSucc.

LaTeX

$$$\\mathrm{Fin.init}\\ (\\lambda k. q\\ k) = (\\lambda k. q\\ k.castSucc)$$$

Lean4

theorem init_def {q : ∀ i, α i} : (init fun k : Fin (n + 1) ↦ q k) = fun k : Fin n ↦ q k.castSucc :=
  rfl

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