continuousOn_multiset_prod — Mathlib

English

If for every i, i ∈ s implies f_i is continuous on t, then a ↦ (s.map f_i a).prod is continuous on t.

Русский

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

LaTeX

$$$\\forall i, \\; i \\in s \\Rightarrow \\text{ContinuousOn}(f i, t) \\Rightarrow \\text{ContinuousOn}\\left(a \\mapsto (s.map (\\lambda i, f i a)).prod, t\\right)$$$

Lean4

@[to_additive]
theorem continuousOn_multiset_prod {f : ι → X → M} (s : Multiset ι) {t : Set X} :
    (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => (s.map fun i => f i a).prod) t :=
  by
  rcases s with ⟨l⟩
  simpa using continuousOn_list_prod l

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