condExpInd_smul' — Mathlib

English

For a scalar c ∈ 𝕜, condExpInd commutes with multiplication by c: condExpInd F hm μ s (c • x) = c • condExpInd F hm μ s x.

Русский

Для скаляра c ∈ 𝕜 condExpInd commutes with умножение на c: condExpInd F hm μ s (c · x) = c · condExpInd F hm μ s x.

LaTeX

$$$ condExpInd\; F\; hm\; \mu\; s\; (c \cdot x) = c \cdot condExpInd\; F\; hm\; \mu\; s\; x,$$

Lean4

theorem condExpInd_smul' [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (c : 𝕜) (x : F) :
    condExpInd F hm μ s (c • x) = c • condExpInd F hm μ s x :=
  condExpIndL1_smul' c x

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