Theorems · Theorem · measure theory

Measurable.fun_neg

∀ {G : Type u_2} {α : Type u_3} [inst : Neg G] [inst_1 : MeasurableSpace G] [MeasurableNeg G] {m : MeasurableSpace α}
  {f : α → G}, Measurable f → Measurable fun i => -f i

Defined in

Mathlib.MeasureTheory.Group.Arithmetic

Cited by

7 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

NegMeasurableSpaceMeasurableNeg