condExpL1_sub — Mathlib

English

For integrable f and g with values in E, condExpL1 hm μ (f+g) equals the sum of condExpL1 hm μ f and condExpL1 hm μ g.

Русский

Для интегрируемых f и g в E выполняется condExpL1 hm μ (f+g) = condExpL1 hm μ f + condExpL1 hm μ g.

LaTeX

$$$condExpL1 hm μ (f+g) = condExpL1 hm μ f + condExpL1 hm μ g$$$

Lean4

theorem condExpL1_sub (hf : Integrable f μ) (hg : Integrable g μ) :
    condExpL1 hm μ (f - g) = condExpL1 hm μ f - condExpL1 hm μ g :=
  setToFun_sub _ hf hg

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