continuousOn_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]
theorem continuousOn_finset_prod {f : ι → X → M} (s : Finset ι) {t : Set X} :
    (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => ∏ i ∈ s, f i a) t :=
  continuousOn_multiset_prod _

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