functorObj — Mathlib

English

Define the sequential product functorObj M N by taking at level n the (ordered) product of M_i for i < n and N_i for i ≥ n. It is the canonical construction of the tower of products with a split between the initial and tail parts.

Русский

Определим последовательный произведение functorObj M N так, что на уровне n берём произведение объектов M_i для i < n и N_i для i ≥ n. Это каноническая конструкция цепи произведений с разрезом между начальной и хвостовой частями.

LaTeX

$$$\\mathrm{functorObj}\\ M\\ N\\ n = \\prod^\\circ_{m:\\mathbb{N}} (\\text{if } m < n \\text{ then } M_m \\text{ else } N_m)$$$

Lean4

/-- The product of the `m` first objects of `M` and the rest of the rest of `N` -/
noncomputable def functorObj : ℕ → C := fun n ↦ ∏ᶜ (fun m ↦ if _ : m < n then M m else N m)

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