Theorems · Definition · Lie groups

ContinuousMap.mulLeft

{X : Type u_5} → [inst : TopologicalSpace X] → [inst_1 : Mul X] → [SeparatelyContinuousMul X] → X → C(X, X)

The continuous map fun y => x * y

Defined in

Mathlib.Topology.Algebra.Monoid

Cited by

3 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

TopologicalSpaceMulSeparatelyContinuousMul