neg_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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