prod — Mathlib

English

If f is Multipliable on β×γ, then the iterated product over b and c equals the product over p in β×γ: ∏' p, f p = ∏' b (c), f(b,c).

Русский

Если функция f на β×γ совмножима, то повторное произведение по координатам равно произведению по всем парам.

LaTeX

$$$\\prod' p, f p = \\prod' b\\,(c), f(\\langle b,c\\rangle)$$$

Lean4

@[to_additive Summable.prod]
theorem prod {f : β × γ → α} (h : Multipliable f) : Multipliable fun b ↦ ∏' c, f (b, c) :=
  ((Equiv.sigmaEquivProd β γ).multipliable_iff.mpr h).sigma

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