instMul — Mathlib

English

Pointwise multiplication defines a multiplication on bounded continuous maps.

Русский

Покоординатное умножение задаёт умножение на ограниченно непрерывные отображения.

LaTeX

$$$\\text{Mul}(\\alpha \\to^\\mathrm{b} R)$$$

Lean4

@[to_additive]
instance instMul [Mul R] [BoundedMul R] [ContinuousMul R] : Mul (α →ᵇ R) where
  mul f
    g :=
    { toFun := fun x ↦ f x * g x
      continuous_toFun := f.continuous.mul g.continuous
      map_bounded' := mul_bounded_of_bounded_of_bounded (map_bounded f) (map_bounded g) }

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