Continuous nonnegative scalar multiplication

instance instContinuousConstSMulSubtypeLeOfNat {R : Type u_1} {α : Type u_2} [Semiring R] [PartialOrder R] [SMul R α] [TopologicalSpace α] [ContinuousConstSMul R α] : ContinuousConstSMul { r : R // 0 ≤ r } α

instance instContinuousSMulSubtypeLeOfNat {R : Type u_1} {α : Type u_2} [Semiring R] [PartialOrder R] [SMul R α] [TopologicalSpace α] [TopologicalSpace R] [ContinuousSMul R α] : ContinuousSMul { r : R // 0 ≤ r } α