condExpIndL1Fin_smul — Mathlib

English

If μ[s] = ∞, then condExpIndL1 hm μ s x = 0.

Русский

Если μ[s] = ∞, то condExpIndL1 hm μ s x = 0.

LaTeX

$$$condExpIndL1_of_measure_eq_top hm μ s x = 0$$$

Lean4

theorem condExpIndL1Fin_smul (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (c : ℝ) (x : G) :
    condExpIndL1Fin hm hs hμs (c • x) = c • condExpIndL1Fin hm hs hμs x :=
  by
  ext1
  grw [Lp.coeFn_smul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndSMul_smul,
    Lp.coeFn_smul]

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