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