instMul

Mathlib.MeasureTheory.Function.AEEqFun

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AEEqFun.instMul

English

The product of two Mk-functions corresponds to Mk of the product: (mk f hf) * (mk g hg) = mk (f g) (hf.mul hg).

Русский

Произведение двух функций Mk соответствует Mk от произведения: (mk f hf) * (mk g hg) = mk (f · g) (hf.mul hg).

LaTeX

$$$ (mk f hf) * (mk g hg) = mk (f \cdot g) (hf.\text{mul} hg) $$$

Lean4

@[to_additive]
instance instMul : Mul (α →ₘ[μ] γ) :=
  ⟨comp₂ (· * ·) continuous_mul⟩

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

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

Разделы

Аффилиация

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