theorem MeasureTheory.Measure.map_prod_comap_swap {Ω : Type u_1} {α : Type u_2} {γ : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace γ] {X : Ω → α} {Z : Ω → γ} (hX : Measurable X) (hZ : Measurable Z) (μ : Measure Ω) : comap Prod.swap (map (fun (ω : Ω) => (X ω, Z ω)) μ) = map (fun (ω : Ω) => (Z ω, X ω)) μ

The law of $(X, Z)$ is the image of the law of $(Z,X)$.

theorem MeasureTheory.Measure.prod_apply_singleton {α : Type u_5} {β : Type u_6} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} (μ : Measure α) (ν : Measure β) [SigmaFinite ν] (x : α × β) : (μ.prod ν) {x} = μ {x.1} * ν {x.2}

theorem MeasureTheory.Measure.prod_real_apply_singleton {α : Type u_5} {β : Type u_6} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} (μ : Measure α) (ν : Measure β) [SigmaFinite ν] (x : α × β) : (μ.prod ν).real {x} = μ.real {x.1} * ν.real {x.2}

theorem MeasureTheory.Measure.prod_of_full_measure_finset {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [SigmaFinite ν] {A : Finset α} {B : Finset β} (hA : μ (↑A)ᶜ = 0) (hB : ν (↑B)ᶜ = 0) : (μ.prod ν) (↑(A ×ˢ B))ᶜ = 0

instance instIsZeroOrProbabilityMeasureProdProd_pFR {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.IsZeroOrProbabilityMeasure μ] {ν : MeasureTheory.Measure β} [MeasureTheory.IsZeroOrProbabilityMeasure ν] : MeasureTheory.IsZeroOrProbabilityMeasure (μ.prod ν)