Theorems · Definition · measure theory

MeasureTheory.DominatedFinMeasAdditive

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

A FinMeasAdditive set function whose norm on every set is less than the measure of the set (up to a multiplicative constant).

Defined in

Mathlib.MeasureTheory.Integral.FinMeasAdditive

Cited by

138 results in Mathlib

Foundations

Depth 171 from the axioms, rests on 4,591 definitions · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddCommGroup