condExpL1_smul — Mathlib

English

For any scalar c in 𝕜 and function f, condExpL1 hm μ (c • f) = c • condExpL1 hm μ f.

Русский

Для скаляра c∈𝕜 и функции f имеем condExpL1 hm μ (c • f) = c • condExpL1 hm μ f.

LaTeX

$$$condExpL1 hm μ (c \cdot f) = c \cdot condExpL1 hm μ f$$$

Lean4

theorem condExpL1_smul (c : 𝕜) (f : α → F') : condExpL1 hm μ (c • f) = c • condExpL1 hm μ f :=
  by
  refine setToFun_smul _ ?_ c f
  exact fun c _ x => condExpInd_smul' c x

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