comp_tail

Mathlib.Data.Fin.Tuple.Basic

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

English

Composition with tail commutes: g ∘ tail q = tail (g ∘ q).

Русский

Сочетание со хвостом сохраняется: g ∘ tail q = tail (g ∘ q).

LaTeX

$$$g \\circ \\mathrm{tail}(q) = \\mathrm{tail}(g \\circ q)$$$

Lean4

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

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

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

Разделы

Аффилиация

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