Theorems · Theorem · general topology

IsUniformInducing.uniformContinuousConstSMul

∀ {M : Type v} {X : Type x} {Y : Type y} [inst : UniformSpace X] [inst_1 : UniformSpace Y] [inst_2 : SMul M X]
  [inst_3 : SMul M Y] [UniformContinuousConstSMul M Y] {f : X → Y},
  IsUniformInducing f → (∀ (c : M) (x : X), f (c • x) = c • f x) → UniformContinuousConstSMul M 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

UniformSpaceUniformSpaceSMulSMulUniformContinuousConstSMul