Theorems · Definition · measure theory

MeasureTheory.FinMeasAdditive

{α : Type u_1} → {β : Type u_7} → [AddMonoid β] → {x : MeasurableSpace α} → MeasureTheory.Measure α → (Set α → β) → Prop

A set function is FinMeasAdditive if its value on the union of two disjoint measurable sets with finite measure is the sum of its values on each set.

Defined in

Mathlib.MeasureTheory.Integral.FinMeasAdditive

Cited by

34 results in Mathlib

Foundations

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

Assumes

AddMonoid