functorObj_eq_neg — Mathlib

English

Let M, N be two sequences of objects in a category. For the nth tail object functorObj M N n, whenever m ≥ n the m-th component equals N_m; i.e., the tail selects the N-part from position n onward.

Русский

Пусть M, N — две последовательности объектов в категории. Для n-го хвостового объекта functorObj M N n, при любом m, удовлетворяющем m ≥ n, m-й компонент равен N_m; т.е. хвост выбирает часть, соответствующую N начиная с позиции n.

LaTeX

$$$\\forall n,m:\\mathbb{N},\\; m \\ge n \\Rightarrow (\\mathrm{functorObj}\\ M\\ N\\ n)_m = N_m$$$

Lean4

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

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