instMulActionUniformOnFun — Mathlib

English

If M is a monoid with a MulAction on β, then there is a MulAction M on UniformOnFun α β 𝔖, defined pointwise.

Русский

Пусть M — моноид с действием на β; тогда на UniformOnFun α β 𝔖 есть действие M, определяемое по точке.

LaTeX

$$$\text{MulAction } M\; (\mathrm{UniformOnFun} \; α \; β \; 𝔖).$$$

Lean4

instance {M : Type*} [Monoid M] [MulAction M β] : MulAction M (α →ᵤ[𝔖] β) :=
  Pi.mulAction _

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