instMonoidUniformOnFun

Mathlib.Topology.Algebra.UniformConvergence

URI: https://scilib.ai/kg/mathlib#instMonoidUniformOnFun

English

If β is a Monoid, then the space UniformOnFun α β 𝓢 is a Monoid under pointwise multiplication.

Русский

Если β — моноид, то UniformOnFun α β 𝓢 образует моноид под покомпонентным умножением.

LaTeX

$$$[Monoid\ \beta] \Rightarrow [Monoid\ (UniformOnFun\ α\beta\ 𝓢)]$$$

Lean4

@[to_additive]
instance [Monoid β] : Monoid (α →ᵤ[𝔖] β) :=
  Pi.monoid

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru