Theorems · Definition · measure theory

MeasureTheory.Measure.toBoxAdditive

{ι : Type u_1} →
  [Finite ι] →
    (μ : MeasureTheory.Measure (ι → ℝ)) → [MeasureTheory.IsLocallyFiniteMeasure μ] → BoxIntegral.BoxAdditiveMap ι ℝ ⊤

If μ is a locally finite measure on ℝⁿ, then fun J ↦ μ.real J is a box-additive function.

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Measure

Cited by

22 results in Mathlib

Foundations

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

Assumes

FiniteMeasureTheory.IsLocallyFiniteMeasure