ι : Sort ?u.29067
M : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace M
inst✝ : SMul M X
ts : Set (TopologicalSpace X)
h : ∀ (t : TopologicalSpace X), t ∈ ts → ContinuousSMul M X
⊢ Continuous fun p => p.fst • p.snd
ι : Sort ?u.29067
M : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace M
inst✝ : SMul M X
ts : Set (TopologicalSpace X)
h : ∀ (t : TopologicalSpace X), t ∈ ts → ContinuousSMul M X
⊢ Continuous fun p => p.fst • p.snd
rw [← (@sInf_singleton _ _ ‹TopologicalSpace M›:)]
no goals
ι : Sort ?u.29067
M : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace M
inst✝ : SMul M X
ts : Set (TopologicalSpace X)
h : ∀ (t : TopologicalSpace X), t ∈ ts → ContinuousSMul M X
⊢ Continuous fun p => p.fst • p.snd
exact
  continuous_sInf_rng.2 fun t ht =>
    continuous_sInf_dom₂ (Eq.refl _) ht
      (@ContinuousSMul.continuous_smul _ _ _ _ t (h t ht))