continuousConstSMul — Mathlib

English

The map y ↦ yx is a continuous endomorphism of X for fixed x in a topological space with a monoid structure.

Русский

Для фиксированного x отображение y ↦ yx непрерывно как отображение X → X при монодной структуре пространства.

LaTeX

$$$\\text{ContinuousMap.mulRight}(x) : X \\to X$, $y \\mapsto y x$ непрерывно$$

Lean4

@[to_additive]
instance (priority := 100) continuousConstSMul : ContinuousConstSMul M X where
  continuous_const_smul _ := continuous_smul.comp (continuous_const.prodMk continuous_id)

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