case mk
ι : Type u_1
α : Type ?u.433203
X : Type u_2
M : Type u_3
N : Type ?u.433212
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
t : Set X
l : List ι
⊢ (∀ (i : ι), i ∈ Quot.mk Setoid.r l → ContinuousOn (f i) t) →
    ContinuousOn (fun a => Multiset.prod (Multiset.map (fun i => f i a) (Quot.mk Setoid.r l))) t
ι : Type u_1
α : Type ?u.433203
X : Type u_2
M : Type u_3
N : Type ?u.433212
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
t : Set X
⊢ (∀ (i : ι), i ∈ s → ContinuousOn (f i) t) → ContinuousOn (fun a => Multiset.prod (Multiset.map (fun i => f i a) s)) t
rcases s with ⟨l⟩
no goals
case mk
ι : Type u_1
α : Type ?u.433203
X : Type u_2
M : Type u_3
N : Type ?u.433212
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
t : Set X
l : List ι
⊢ (∀ (i : ι), i ∈ Quot.mk Setoid.r l → ContinuousOn (f i) t) →
    ContinuousOn (fun a => Multiset.prod (Multiset.map (fun i => f i a) (Quot.mk Setoid.r l))) t
simpa using continuousOn_list_prod l