Theorems · Definition · measure theory

MeasureTheory.piPremeasure

{ι : Type u_1} →
  {α : ι → Type u_3} → [Fintype ι] → ((i : ι) → MeasureTheory.OuterMeasure (α i)) → Set ((i : ι) → α i) → ENNReal

An upper bound for the measure in a finite product space. It is defined by taking the image of the set under all projections, and taking the product of the measures of these images. For measurable boxes it is equal to the correct measure.

Defined in

Mathlib.MeasureTheory.Constructions.Pi

Cited by

6 results in Mathlib

Foundations

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

Assumes

Fintype