Theorems · Theorem · Lie groups

ContinuousMap.mulLeft_mul

∀ {X : Type u_6} [inst : Semigroup X] [inst_1 : TopologicalSpace X] [inst_2 : SeparatelyContinuousMul X] (x y : X),
  ContinuousMap.mulLeft (x * y) = (ContinuousMap.mulLeft x).comp (ContinuousMap.mulLeft y)

Defined in

Mathlib.Topology.Algebra.Monoid

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound

Assumes

SemigroupTopologicalSpaceSeparatelyContinuousMul