Theorems · Theorem · general topology

smul_uniformity

∀ {M : Type v} {X : Type x} [inst : UniformSpace X] [inst_1 : Group M] [inst_2 : MulAction M X]
  [UniformContinuousConstSMul M X] (c : M), c • uniformity X = uniformity X

Defined in

Mathlib.Topology.Algebra.UniformMulAction

Cited by

0 results in Mathlib

Foundations

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

Assumes

UniformSpaceGroupMulActionUniformContinuousConstSMul