smul — Mathlib

English

The continuous map mulLeft x is the map y ↦ x y, giving left multiplication by x as a continuous endomorphism.

Русский

Карта mulLeft x задаёт отображение слева умножения на x, непрерывна как эндоморфизм на X.

LaTeX

$$$\\text{ContinuousMap.mulLeft}(x) : X \\to X$, $y \\mapsto x y$$$

Lean4

@[to_additive (attr := fun_prop)]
theorem smul (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun x => f x • g x) s := fun x hx =>
  (hf x hx).smul (hg x hx)

Похожие утверждения