tprod_apply — Mathlib

English

If f is Multipliable, then the value of the tprod over i evaluated at x equals the tprod over i of the x-slice: (tprod f i) x = tprod (f i x).

Русский

Значение tprod над i в точке x равно tprod по i отрезку: (tprod f i) x = tprod (f i x).

LaTeX

$$$(\\prod' [L] i, f i) x = \\prod' [L] i, f i x$$$

Lean4

@[to_additive]
theorem tprod_apply [L.NeBot] [∀ x, T2Space (X x)] {f : ι → ∀ x, X x} {x : α} (hf : Multipliable f L) :
    (∏'[L] i, f i) x = ∏'[L] i, f i x :=
  (Pi.hasProd.mp hf.hasProd x).tprod_eq.symm

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