instance MeasureTheory.Measure.instIsProbabilityMeasureForallPi_pFR {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), IsProbabilityMeasure (μ i)] : IsProbabilityMeasure (Measure.pi μ)

@[simp]

theorem MeasureTheory.Measure.pi_pi_set {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), IsProbabilityMeasure (μ i)] (t : Set ι) [DecidablePred fun (x : ι) => x ∈ t] (s : (i : ι) → Set (α i)) : (Measure.pi μ) (t.pi s) = ∏ i ∈ Finset.filter (fun (x : ι) => x ∈ t) Finset.univ, (μ i) (s i)

@[simp]

theorem MeasureTheory.Measure.pi_pi_finset {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), IsProbabilityMeasure (μ i)] (t : Finset ι) (s : (i : ι) → Set (α i)) : (Measure.pi μ) ((↑t).pi s) = ∏ i ∈ t, (μ i) (s i)

@[simp]

theorem MeasureTheory.Measure.pi_eval_preimage {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), IsProbabilityMeasure (μ i)] (i : ι) (s : Set (α i)) : (Measure.pi μ) (Function.eval i ⁻¹' s) = (μ i) s

theorem MeasureTheory.Measure.map_eval_pi {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), IsProbabilityMeasure (μ i)] (i : ι) : map (Function.eval i) (Measure.pi μ) = μ i