continuous_multiset_prod — Mathlib

English

If every f_i is continuous on X, then the map a ↦ (s.map f_i a).prod is continuous, where s is a fixed multiset of indices.

Русский

Если каждый f_i непрерывна на X, то отображение a ↦ (суммируемый по i в s) ∏ f_i(a) непрерывно.

LaTeX

$$$\\forall s,\\ (\\forall i \\in s,\\ Continuous (f i)) \\Rightarrow \\text{Continuous}\\bigl(a \\mapsto (s.map (\\lambda i, f i a)).prod\\bigr)$$$

Lean4

@[to_additive (attr := continuity, fun_prop)]
theorem continuous_multiset_prod {f : ι → X → M} (s : Multiset ι) :
    (∀ i ∈ s, Continuous (f i)) → Continuous fun a => (s.map fun i => f i a).prod :=
  by
  rcases s with ⟨l⟩
  simpa using continuous_list_prod l

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