pair — Mathlib

English

Combine two simple functions f : α →ₛ β and g : α →ₛ γ into a simple function α →ₛ β × γ by pairing the outputs.

Русский

Сложим две простые функции f : α →ₛ β и g : α →ₛ γ в простую функцию α →ₛ β × γ, спаривая выходы.

LaTeX

$$$$ \\text{pair } f\\; g : α \\to_\\mathrm{SimpleFunc} (β \\times γ) = (f.map \\mathrm{Prod.mk}).seq g. $$$$

Lean4

/-- Combine two simple functions `f : α →ₛ β` and `g : α →ₛ β`
into `fun a => (f a, g a)`. -/
def pair (f : α →ₛ β) (g : α →ₛ γ) : α →ₛ β × γ :=
  (f.map Prod.mk).seq g

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