instSMulCommClassAEEqFun_1

Mathlib.MeasureTheory.Function.AEEqFun.DomAct

URI: https://scilib.ai/kg/mathlib#DomMulAct.instSMulCommClassAEEqFun_1

English

A second variant of the commuting Smul class for AEEqFun under relaxed assumptions.

Русский

Второй вариант свойства коммутирования действия для AEEqFun при ослабленных предположениях.

LaTeX

$$Instance: SMulCommClass N (DomMulAct M) (AEEqFun α β μ)$$

Lean4

instance [SMul N β] [ContinuousConstSMul N β] : SMulCommClass N Mᵈᵐᵃ (α →ₘ[μ] β) :=
  .symm _ _ _

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

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

Разделы

Аффилиация

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