Theorems · Theorem · general topology

uniformContinuousConstSMul_of_continuousConstSMul

∀ (R : Type u) (M : Type v) [inst : AddGroup M] [inst_1 : DistribSMul R M] [inst_2 : UniformSpace M]
  [IsUniformAddGroup M] [ContinuousConstSMul R M], UniformContinuousConstSMul R M

A DistribSMul that is continuous on a uniform group is uniformly continuous. This can't be an instance due to it forming a loop with UniformContinuousConstSMul.instContinuousConstSMul

Defined in

Mathlib.Topology.Algebra.UniformMulAction

Cited by

0 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupDistribSMulUniformSpaceIsUniformAddGroupContinuousConstSMul