English
If an infinite product of functions f: γ → C(α, β) converges to g in the compact-open topology, then for each x ∈ α, the pointwise products converge to g(x).
Русский
Если бесконечный произведение функций сходится к g в компактно-открытой топологии, то по каждой точке x произведение сходится к g(x).
LaTeX
$$$\forall x\in α,\ HasProd f g L \Rightarrow HasProd (\lambda i, f(i)(x)) (g(x)) L$$$
Lean4
/-- If an infinite product of functions in `C(α, β)` converges to `g`
(for the compact-open topology), then the pointwise product converges to `g x` for all `x ∈ α`. -/
@[to_additive /-- If an infinite sum of functions in `C(α, β)` converges to `g` (for the compact-open topology),
then the pointwise sum converges to `g x` for all `x ∈ α`. -/
]
theorem hasProd_apply {γ : Type*} [CommMonoid β] [ContinuousMul β] {f : γ → C(α, β)} {g : C(α, β)}
{L : SummationFilter γ} (hf : HasProd f g L) (x : α) : HasProd (fun i : γ => f i x) (g x) L :=
by
let ev : C(α, β) →* β := (Pi.evalMonoidHom _ x).comp coeFnMonoidHom
exact hf.map ev (continuous_eval_const x)
