ι : Type ?u.456770
α : Type ?u.456773
X : Type ?u.456776
M : Type u_1
N : Type ?u.456782
inst✝¹ : TopologicalSpace X
ι' : Sort u_2
inst✝ : Mul M
ts : ι' → TopologicalSpace M
h' : ∀ (i : ι'), ContinuousMul M
⊢ ContinuousMul M
ι : Type ?u.456770
α : Type ?u.456773
X : Type ?u.456776
M : Type u_1
N : Type ?u.456782
inst✝¹ : TopologicalSpace X
ι' : Sort u_2
inst✝ : Mul M
ts : ι' → TopologicalSpace M
h' : ∀ (i : ι'), ContinuousMul M
⊢ ContinuousMul M
rw [← sInf_range]
no goals
ι : Type ?u.456770
α : Type ?u.456773
X : Type ?u.456776
M : Type u_1
N : Type ?u.456782
inst✝¹ : TopologicalSpace X
ι' : Sort u_2
inst✝ : Mul M
ts : ι' → TopologicalSpace M
h' : ∀ (i : ι'), ContinuousMul M
⊢ ContinuousMul M
exact continuousMul_sInf (Set.forall_range_iff.mpr h')