Documentation

Mathlib.Topology.Algebra.Order.Module

Continuous nonnegative scalar multiplication #

source
📐 coverage
instance instContinuousConstSMulSubtypeLeOfNat {R : Type u_1} {α : Type u_2} [Semiring R] [PartialOrder R] [SMul R α] [TopologicalSpace α] [ContinuousConstSMul R α] :
ContinuousConstSMul { r : R // 0 ≤ r } α
source
📐 coverage
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 } α