prod — Mathlib

English

The map into a product type built from maps into each component is defined by Pi.prod f g i = (f i, g i).

Русский

Отображение в произведение из карт к каждому компоненту задаётся как Pi.prod f g i = (f i, g i).

LaTeX

$$$\Pi.prod\ f\ g\ i = (f i, g i)$$$

Lean4

/-- The mapping into a product type built from maps into each component. -/
@[simp]
protected def prod {α β : ι → Type*} (f : ∀ i, α i) (g : ∀ i, β i) (i : ι) : α i × β i :=
  (f i, g i)

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