coeFn_smul

Mathlib.MeasureTheory.Function.LpSpace.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Lp.coeFn_smul

English

The scalar multiplication commutes with the equivalence class representative for Lp.

Русский

Умножение на скаляр commuting с представителем классов эквивалентности Lp.

LaTeX

$$$\text{coeFn\_smul}$ равенство$$

Lean4

theorem coeFn_smul (c : 𝕜) (f : Lp E p μ) : ⇑(c • f) =ᵐ[μ] c • ⇑f :=
  AEEqFun.coeFn_smul _ _

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

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

Разделы

Аффилиация

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