neg_right — Mathlib

English

If f and g are conditionally independent, then f is independent of -g as well.

Русский

Если выполнена условная независимость между f и g, то независимы также f и −g.

LaTeX

$$$\operatorname{CondIndepFun} \; m' \; hm' \; f \; g \; μ \Rightarrow \operatorname{CondIndepFun} \; m' \; hm' \; f \; (-g) \; μ$$$

Lean4

theorem neg_right {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [Neg β'] [MeasurableNeg β']
    (hfg : CondIndepFun m' hm' f g μ) : CondIndepFun m' hm' f (-g) μ :=
  hfg.comp measurable_id measurable_neg

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