neg_right — Mathlib

English

If f and g are independent, then f and −g are independent (assuming a negation operation on the codomain).

Русский

Если f и g независимы, то f и −g независимы (при условии применения отрицания к кодомену).

LaTeX

$$$ \\operatorname{IndepFun}(f,g,\\mu) \\rightarrow \\operatorname{IndepFun}(f,-g,\\mu) $$$

Lean4

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

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