Theorems · Theorem · probability

MeasureTheory.inducedFamily_Iic

∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (μ : (n : ℕ) → MeasureTheory.Measure ((i : ↥(Finset.Iic n)) → X ↑i)) (n : ℕ),
  MeasureTheory.inducedFamily μ (Finset.Iic n) = μ n

Given a family of measures μ : (n : ℕ) → Measure (Π i : Iic n, X i), the induced family equals μ over the intervals Iic n.

Defined in

Mathlib.Probability.Kernel.IonescuTulcea.Traj

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpace