Theorems · Theorem · probability

ProbabilityTheory.IndepFun.neg_left

∀ {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → β}
  {g : Ω → β'} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [inst : Neg β] [MeasurableNeg β],
  ProbabilityTheory.IndepFun f g μ → ProbabilityTheory.IndepFun (-f) g μ

Defined in

Mathlib.Probability.Independence.Basic

Cited by

0 results in Mathlib

Foundations

Depth 181 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NegMeasurableNeg