Theorems · Definition · measure theory

MeasureTheory.IsProjectiveMeasureFamily

{ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → MeasurableSpace (α i)] → ((J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)) → Prop

A family of measures indexed by finite sets of ι is projective if, for finite sets J ⊆ I, the projection from ∀ i : I, α i to ∀ i : J, α i maps P I to P J.

Defined in

Mathlib.MeasureTheory.Constructions.Projective

Cited by

27 results in Mathlib

Foundations

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

Assumes

MeasurableSpace