prod_factor — Mathlib

English

If f is Multipliable on β × γ, then for each b the function c ↦ f(b,c) is Multipliable.

Русский

Если f умножаемо на β×γ, то для каждого b функция c ↦ f(b,c) умножаема.

LaTeX

$$$$ \forall b, \mathrm{Multipliable}(\lambda c, f(b,c)). $$$$

Lean4

@[to_additive Summable.prod_factor]
theorem prod_factor {f : β × γ → α} (h : Multipliable f) (b : β) : Multipliable fun c ↦ f (b, c) :=
  h.comp_injective fun _ _ h ↦ (Prod.ext_iff.1 h).2

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