comp_init

Mathlib.Data.Fin.Tuple.Basic

URI: https://scilib.ai/kg/mathlib#Fin.comp_init

English

Composition with init distributes over a map g: g ∘ init q = init (g ∘ q).

Русский

Композиция с init распространяется в отношении отображения: g ∘ init q = init (g ∘ q).

LaTeX

$$$g\\\\circ\\\\operatorname{init} q = \\\\operatorname{init}(g\\\\circ q)$$$

Lean4

theorem comp_init {α : Sort*} {β : Sort*} (g : α → β) (q : Fin n.succ → α) : g ∘ init q = init (g ∘ q) :=
  by
  ext j
  simp [init]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru