∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → MeasureTheory.Measure (X n))
  [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] {A : Set ((n : ℕ) → X n)},
  A ∈ MeasureTheory.measurableCylinders X → (MeasureTheory.piContent μ) A = (MeasureTheory.Measure.infinitePiNat μ) A