tprod_apply — Mathlib

English

For a suitable summation filter L and Multipliable f, the limit of the tprod equals the evaluation at x: ∏'[L] f_i x = (∏'[L] f_i) x.

Русский

При надлежащем L переход к предельному произведению эквивалентен точечному произведению: ∏'[L] f_i x = (∏'[L] f_i) x.

LaTeX

$$$\prod'_{L} i:\gamma, f(i)(x) = (\prod'_{L} i:\gamma, f(i))(x)$$$

Lean4

@[to_additive]
theorem tprod_apply [T2Space β] [CommMonoid β] [ContinuousMul β] {γ : Type*} {f : γ → C(α, β)} {L : SummationFilter γ}
    (hf : Multipliable f L) [L.NeBot] (x : α) : ∏'[L] i : γ, f i x = (∏'[L] i : γ, f i) x :=
  (hasProd_apply hf.hasProd x).tprod_eq

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