mul_eq_map₂ — Mathlib

English

The pointwise product of two simple functions equals the map of their pair to the product: f * g = (pair f g).map (λ p, p.1 * p.2).

Русский

Пойнтовый произведение двух простых функций равно отображению пары функций в их произведение: f * g = (pair f g).map (λ p, p.1 * p.2).

LaTeX

$$$f * g = (\\text{pair } f\\ g).\\text{map } (\\lambda p:(\\beta \\times \\beta), p.1 \\cdot p.2).$$$

Lean4

@[to_additive]
theorem mul_eq_map₂ [Mul β] (f g : α →ₛ β) : f * g = (pair f g).map fun p : β × β => p.1 * p.2 :=
  rfl

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