continuous_finset_prod — Mathlib

English

If every f_i is continuous on t for i in a finite set s, then a ↦ ∏_{i∈s} f_i(a) is continuous on t.

Русский

Если для каждого i∈s отображение f_i непрерывно на t, то a ↦ ∏_{i∈s} f_i(a) непрерывно на t.

LaTeX

$$$\\forall i \\in s,\\ ContinuousOn (f i)\\ t\\;\\Rightarrow\\; \\text{ContinuousOn}\\left(a \\mapsto \\prod_{i \\in s} f_i(a) , t\\right)$$

Lean4

@[to_additive (attr := continuity, fun_prop)]
theorem continuous_finset_prod {f : ι → X → M} (s : Finset ι) :
    (∀ i ∈ s, Continuous (f i)) → Continuous fun a => ∏ i ∈ s, f i a :=
  continuous_multiset_prod _

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