instSMulCommClassUniformOnFun

Mathlib.Topology.Algebra.UniformConvergence

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

English

If SMulCommClass M N β holds, then SMulCommClass M N (UniformOnFun α β 𝔖) holds.

Русский

Если SMulCommClass M N β, то SMulCommClass M N (UniformOnFun α β 𝔖).

LaTeX

$$$SMulCommClass\; M\; N\; β \rightarrow SMulCommClass\; M\; N\; (UniformOnFun \; α \; β \; 𝔖).$$$

Lean4

instance {M N : Type*} [SMul M β] [SMul N β] [SMulCommClass M N β] : SMulCommClass M N (α →ᵤ[𝔖] β) :=
  Pi.smulCommClass

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

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

Разделы

Аффилиация

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