ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : MeasureTheory.IntegrableOn f s μ<GOAL>0 < μ {x | x ∈ s ∧ ⨍ (a : α) in s, f a ∂μ ≤ f x}
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : MeasureTheory.IntegrableOn f s μ<GOAL>∃ x ∈ s, f x ≤ ⨍ (a : α) in s, f a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : MeasureTheory.IntegrableOn f s μ<GOAL>∃ x ∈ s, ⨍ (a : α) in s, f a ∂μ ≤ f x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : MeasureTheory.Integrable f μ<GOAL>0 < μ {x | f x ≤ ⨍ (a : α), f a ∂μ}
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : MeasureTheory.Integrable f μ<GOAL>0 < μ {x | ⨍ (a : α), f a ∂μ ≤ f x}
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∃ x, f x ≤ ⨍ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∃ x, ⨍ (a : α), f a ∂μ ≤ f x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>N : Set α<VAR>f : α → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : MeasureTheory.Integrable f μ<VAR>hN : μ N = 0<GOAL>∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>N : Set α<VAR>f : α → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : MeasureTheory.Integrable f μ<VAR>hN : μ N = 0<GOAL>∃ x ∉ N, ⨍ (a : α), f a ∂μ ≤ f x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>0 < μ {x | f x ≤ ∫ (a : α), f a ∂μ}
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>0 < μ {x | ∫ (a : α), f a ∂μ ≤ f x}
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∃ x, f x ≤ ∫ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∃ x, ∫ (a : α), f a ∂μ ≤ f x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>N : Set α<VAR>f : α → ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hf : MeasureTheory.Integrable f μ<VAR>hN : μ N = 0<GOAL>∃ x ∉ N, f x ≤ ∫ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>N : Set α<VAR>f : α → ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hf : MeasureTheory.Integrable f μ<VAR>hN : μ N = 0<GOAL>∃ x ∉ N, ∫ (a : α), f a ∂μ ≤ f x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : AEMeasurable f (μ.restrict s)<GOAL>0 < μ {x | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ}
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤<GOAL>0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : AEMeasurable f (μ.restrict s)<GOAL>∃ x ∈ s, f x ≤ ⨍⁻ (a : α) in s, f a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤<GOAL>∃ x ∈ s, ⨍⁻ (a : α) in s, f a ∂μ ≤ f x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ ≠ 0<VAR>hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤<GOAL>0 < μ {x | ⨍⁻ (a : α), f a ∂μ ≤ f x}
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ ≠ 0<VAR>hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤<GOAL>∃ x, ⨍⁻ (a : α), f a ∂μ ≤ f x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ ≠ 0<VAR>hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤<VAR>hN : μ N = 0<GOAL>∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : AEMeasurable f μ<GOAL>0 < μ {x | f x ≤ ⨍⁻ (a : α), f a ∂μ}
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : AEMeasurable f μ<GOAL>∃ x, f x ≤ ⨍⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>N : Set α<VAR>f : α → ℝ≥0∞<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : AEMeasurable f μ<VAR>hN : μ N = 0<GOAL>∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hf : AEMeasurable f μ<GOAL>0 < μ {x | f x ≤ ∫⁻ (a : α), f a ∂μ}
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤<GOAL>0 < μ {x | ∫⁻ (a : α), f a ∂μ ≤ f x}
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hf : AEMeasurable f μ<GOAL>∃ x, f x ≤ ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤<GOAL>∃ x, ∫⁻ (a : α), f a ∂μ ≤ f x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>N : Set α<VAR>f : α → ℝ≥0∞<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hf : AEMeasurable f μ<VAR>hN : μ N = 0<GOAL>∃ x ∉ N, f x ≤ ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>N : Set α<VAR>f : α → ℝ≥0∞<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤<VAR>hN : μ N = 0<GOAL>∃ x ∉ N, ∫⁻ (a : α), f a ∂μ ≤ f x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_4<VAR>a : ι → Set α<VAR>l : Filter ι<VAR>f : α → E<VAR>c : E<VAR>g : ι → α → ℝ<VAR>K : ℝ<VAR>hf : Filter.Tendsto (fun i => ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)<VAR>f_int : ∀ᶠ (i : ι) in l, MeasureTheory.IntegrableOn f (a i) μ<VAR>hg : Filter.Tendsto (fun i => ∫ (y : α), g i y ∂μ) l (𝓝 1)<VAR>g_supp : ∀ᶠ (i : ι) in l, Function.support (g i) ⊆ a i<VAR>g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / (μ (a i)).toReal<GOAL>Filter.Tendsto (fun i => ∫ (y : α), g i y • f y ∂μ) l (𝓝 c)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>hC : IsPiSystem C<VAR>hD : IsPiSystem D<GOAL>IsPiSystem (Set.image2 (fun x x_1 => x ×ˢ x_1) C D)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>hC : IsCountablySpanning C<VAR>hD : IsCountablySpanning D<GOAL>IsCountablySpanning (Set.image2 (fun x x_1 => x ×ˢ x_1) C D)
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>hC : IsCountablySpanning C<VAR>hD : IsCountablySpanning D<GOAL>Prod.instMeasurableSpace = MeasurableSpace.generateFrom (Set.image2 (fun x x_1 => x ×ˢ x_1) C D)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>hC : MeasurableSpace.generateFrom C = inst✝<VAR>hD : MeasurableSpace.generateFrom D = inst✝¹<VAR>h2C : IsCountablySpanning C<VAR>h2D : IsCountablySpanning D<GOAL>MeasurableSpace.generateFrom (Set.image2 (fun x x_1 => x ×ˢ x_1) C D) = Prod.instMeasurableSpace
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<GOAL>MeasurableSpace.generateFrom (Set.image2 (fun x x_1 => x ×ˢ x_1) {s | MeasurableSet s} {t | MeasurableSet t}) = Prod.instMeasurableSpace
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<GOAL>IsPiSystem (Set.image2 (fun x x_1 => x ×ˢ x_1) {s | MeasurableSet s} {t | MeasurableSet t})
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.IsFiniteMeasure ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>Measurable fun x => ν (Prod.mk x ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>Measurable fun x => ν (Prod.mk x ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>Measurable fun y => μ ((fun x => (x, y)) ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<GOAL>Measurable fun x => MeasureTheory.Measure.map (Prod.mk x) ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<GOAL>Measurable fun y => MeasureTheory.Measure.map (fun x => (x, y)) μ
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f : α → β<VAR>g : γ → δ<VAR>hg : MeasurableEmbedding g<VAR>hf : MeasurableEmbedding f<GOAL>MeasurableEmbedding fun x => (g x.1, f x.2)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>MeasurableSingletonClass α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>x : α<VAR>f : γ → β<VAR>hf : MeasurableEmbedding f<GOAL>MeasurableEmbedding fun y => (x, f y)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSingletonClass α<VAR>x : α<GOAL>MeasurableEmbedding (Prod.mk x)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>MeasurableSingletonClass α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : γ → β<VAR>hf : MeasurableEmbedding f<VAR>x : α<GOAL>MeasurableEmbedding fun y => (f y, x)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSingletonClass α<VAR>x : α<GOAL>MeasurableEmbedding fun y => (y, x)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>f : α × β → ℝ≥0∞<GOAL>Measurable f → Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>f : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<GOAL>Measurable fun x => ∫⁻ (y : β), f x y ∂ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>f : α × β → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Measurable fun y => ∫⁻ (x : α), f (x, y) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>f : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<GOAL>Measurable fun y => ∫⁻ (x : α), f x y ∂μ
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<GOAL>μ.prod ν = μ.bind fun x => MeasureTheory.Measure.map (Prod.mk x) ν
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>MeasureTheory.MeasureSpace α<VAR>MeasureTheory.MeasureSpace β<GOAL>MeasureTheory.volume = MeasureTheory.volume.prod MeasureTheory.volume
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>(μ.prod ν) s = ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>s : Set α<VAR>t : Set β<GOAL>(μ.prod ν) (s ×ˢ t) = μ s * ν t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<GOAL>MeasureTheory.Measure.map Prod.fst (μ.prod ν) = ν Set.univ • μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<GOAL>MeasureTheory.Measure.map Prod.snd (μ.prod ν) = μ Set.univ • ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<VAR>h2s : (μ.prod ν) s ≠ ⊤<GOAL>∀ᵐ (x : α) ∂μ, ν (Prod.mk x ⁻¹' s) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>(μ.prod ν) s = 0 ↔ (fun x => ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>s : Set (α × β)<VAR>h : (μ.prod ν) s = 0<GOAL>(fun x => ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ μ' : MeasureTheory.Measure α<VAR>ν ν' : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite ν'<VAR>h1 : μ ≪ μ'<VAR>h2 : ν ≪ ν'<GOAL>μ.prod ν ≪ μ'.prod ν'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>p : α × β → Prop<VAR>h : ∀ᵐ (z : α × β) ∂μ.prod ν, p z<GOAL>∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, p (x, y)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>f g : α × β → γ<VAR>h : f =ᵐ[μ.prod ν] g<GOAL>∀ᵐ (x : α) ∂μ, Function.curry f x =ᵐ[ν] Function.curry g x
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>f g : α → β → γ<VAR>h : Function.uncurry f =ᵐ[μ.prod ν] Function.uncurry g<GOAL>∀ᵐ (x : α) ∂μ, f x =ᵐ[ν] g x
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>(∀ᵐ (z : α × β) ∂μ.prod ν, z ∈ s) ↔ ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, (x, y) ∈ s
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving Prod.fst (μ.prod ν) μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving Prod.snd (μ.prod ν) ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>s s' : Set α<VAR>t t' : Set β<VAR>hs : s =ᵐ[μ] s'<VAR>ht : t =ᵐ[ν] t'<GOAL>s ×ˢ t =ᵐ[μ.prod ν] s' ×ˢ t'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>s : Set α<VAR>t : Set β<VAR>s_ae_univ : μ sᶜ = 0<VAR>t_ae_univ : ν tᶜ = 0<GOAL>(μ.prod ν) (s ×ˢ t)ᶜ = 0
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>s : Set α<VAR>t : Set β<VAR>s_mble : MeasureTheory.NullMeasurableSet s μ<VAR>t_mble : MeasureTheory.NullMeasurableSet t ν<GOAL>MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>s : Set α<VAR>t : Set β<VAR>h : MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν)<VAR>hs : μ s ≠ 0<GOAL>MeasureTheory.NullMeasurableSet t ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>NeZero μ<VAR>t : Set β<VAR>h : MeasureTheory.NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν)<GOAL>MeasureTheory.NullMeasurableSet t ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>NeZero μ<VAR>t : Set β<GOAL>MeasureTheory.NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν) ↔ MeasureTheory.NullMeasurableSet t ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>NeZero μ<VAR>f : β → γ<GOAL>MeasureTheory.NullMeasurable (f ∘ Prod.snd) (μ.prod ν) ↔ MeasureTheory.NullMeasurable f ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ι : Type u_7<VAR>m : ι → MeasureTheory.Measure α<VAR>μ : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite μ<GOAL>(MeasureTheory.Measure.sum m).prod μ = MeasureTheory.Measure.sum fun i => (m i).prod μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ι' : Type u_7<VAR>Countable ι'<VAR>m : MeasureTheory.Measure α<VAR>m' : ι' → MeasureTheory.Measure β<VAR>∀ (n : ι'), MeasureTheory.SFinite (m' n)<GOAL>m.prod (MeasureTheory.Measure.sum m') = MeasureTheory.Measure.sum fun p => m.prod (m' p)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>Countable ι'<VAR>m : ι → MeasureTheory.Measure α<VAR>m' : ι' → MeasureTheory.Measure β<VAR>∀ (n : ι'), MeasureTheory.SFinite (m' n)<GOAL>(MeasureTheory.Measure.sum m).prod (MeasureTheory.Measure.sum m') = MeasureTheory.Measure.sum fun p => (m p.1).prod (m' p.2)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>hC : MeasurableSpace.generateFrom C = inst✝<VAR>hD : MeasurableSpace.generateFrom D = inst✝¹<VAR>h2C : IsPiSystem C<VAR>h2D : IsPiSystem D<VAR>h3C : μ.FiniteSpanningSetsIn C<VAR>h3D : ν.FiniteSpanningSetsIn D<VAR>μν : MeasureTheory.Measure (α × β)<VAR>h₁ : ∀ s ∈ C, ∀ t ∈ D, μν (s ×ˢ t) = μ s * ν t<GOAL>μ.prod ν = μν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SigmaFinite ν<VAR>μν : MeasureTheory.Measure (α × β)<VAR>h : ∀ (s : Set α) (t : Set β), MeasurableSet s → MeasurableSet t → μν (s ×ˢ t) = μ s * ν t<GOAL>μ.prod ν = μν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<GOAL>MeasureTheory.Measure.map Prod.swap (μ.prod ν) = ν.prod μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<GOAL>MeasureTheory.MeasurePreserving Prod.swap (μ.prod ν) (ν.prod μ)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>(μ.prod ν) s = ∫⁻ (y : β), μ ((fun x => (x, y)) ⁻¹' s) ∂ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>s : Set α<VAR>t : Set β<VAR>h : MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν)<VAR>ht : ν t ≠ 0<GOAL>MeasureTheory.NullMeasurableSet s μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>NeZero ν<VAR>s : Set α<VAR>h : MeasureTheory.NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν)<GOAL>MeasureTheory.NullMeasurableSet s μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>NeZero ν<VAR>s : Set α<GOAL>MeasureTheory.NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν) ↔ MeasureTheory.NullMeasurableSet s μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>NeZero ν<VAR>f : α → γ<GOAL>MeasureTheory.NullMeasurable (f ∘ Prod.fst) (μ.prod ν) ↔ MeasureTheory.NullMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>s : Set α<VAR>t : Set β<VAR>hs : μ s ≠ 0<VAR>ht : ν t ≠ 0<GOAL>MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔ MeasureTheory.NullMeasurableSet s μ ∧ MeasureTheory.NullMeasurableSet t ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>s : Set α<VAR>t : Set β<GOAL>MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔ MeasureTheory.NullMeasurableSet s μ ∧ MeasureTheory.NullMeasurableSet t ν ∨ μ s = 0 ∨ ν t = 0
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>τ : MeasureTheory.Measure γ<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasureTheory.SFinite τ<GOAL>MeasureTheory.Measure.map (⇑MeasurableEquiv.prodAssoc) ((μ.prod ν).prod τ) = μ.prod (ν.prod τ)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>s : Set α<VAR>t : Set β<GOAL>(μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>s : Set α<GOAL>(μ.restrict s).prod ν = (μ.prod ν).restrict (s ×ˢ Set.univ)