tprod_prod — Mathlib

English

If f is Multipliable on β×γ, then the full tprod over p equals the tprod over b and c: ∏' p, f p = ∏' (b) (c), f ⟨b,c⟩.

Русский

Если f совмножима на β×γ, то полное tprod по p равно tprod по b и c.

LaTeX

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

Lean4

@[to_additive Summable.tsum_prod]
protected theorem tprod_prod {f : β × γ → α} (h : Multipliable f) : ∏' p, f p = ∏' (b) (c), f ⟨b, c⟩ :=
  h.tprod_prod' h.prod_factor

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