functorObj_eq_pos

Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.SequentialProduct.functorObj_eq_pos

English

If m < n then the m-th value of the concatenated sequence equals M_m.

Русский

Если m < n, то m-я компонента конкатенированной последовательности равна M_m.

LaTeX

$$$\text{fun i ↦ if } i < n \text{ then } M i \text{ else } N i\; m = M m\quad (m < n)$$$

Lean4

theorem functorObj_eq_pos {n m : ℕ} (h : m < n) : (fun i ↦ if _ : i < n then M i else N i) m = M m :=
  dif_pos h

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

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

Разделы

Аффилиация

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