ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>NormedLatticeAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>↑↑|f| =ᵐ[μ] fun x => |↑↑f x|
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>C : (i : ι) → Set (Set (α i))<VAR>hC : ∀ (i : ι), IsPiSystem (C i)<GOAL>IsPiSystem (Set.univ.pi '' Set.univ.pi C)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>(i : ι) → MeasurableSpace (α i)<GOAL>IsPiSystem (Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s})
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Finite ι<VAR>C : (i : ι) → Set (Set (α i))<VAR>hC : ∀ (i : ι), IsCountablySpanning (C i)<GOAL>IsCountablySpanning (Set.univ.pi '' Set.univ.pi C)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Finite ι<VAR>C : (i : ι) → Set (Set (α i))<VAR>hC : ∀ (i : ι), IsCountablySpanning (C i)<GOAL>MeasurableSpace.pi = MeasurableSpace.generateFrom (Set.univ.pi '' Set.univ.pi C)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Finite ι<VAR>h : (i : ι) → MeasurableSpace (α i)<VAR>C : (i : ι) → Set (Set (α i))<VAR>hC : ∀ (i : ι), MeasurableSpace.generateFrom (C i) = h i<VAR>h2C : ∀ (i : ι), IsCountablySpanning (C i)<GOAL>MeasurableSpace.generateFrom (Set.univ.pi '' Set.univ.pi C) = MeasurableSpace.pi
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Finite ι<VAR>(i : ι) → MeasurableSpace (α i)<GOAL>MeasurableSpace.generateFrom (Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}) = MeasurableSpace.pi
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>m : (i : ι) → MeasureTheory.OuterMeasure (α i)<VAR>s : (i : ι) → Set (α i)<VAR>hs : (Set.univ.pi s).Nonempty<GOAL>MeasureTheory.piPremeasure m (Set.univ.pi s) = ∏ i : ι, (m i) (s i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>m : (i : ι) → MeasureTheory.OuterMeasure (α i)<VAR>s : (i : ι) → Set (α i)<GOAL>MeasureTheory.piPremeasure m (Set.univ.pi s) = ∏ i : ι, (m i) (s i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>m : (i : ι) → MeasureTheory.OuterMeasure (α i)<VAR>s t : Set ((i : ι) → α i)<VAR>h : s ⊆ t<GOAL>MeasureTheory.piPremeasure m s ≤ MeasureTheory.piPremeasure m t
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>m : (i : ι) → MeasureTheory.OuterMeasure (α i)<VAR>s : Set ((i : ι) → α i)<GOAL>MeasureTheory.piPremeasure m (Set.univ.pi fun i => Function.eval i '' s) = MeasureTheory.piPremeasure m s
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>m : (i : ι) → MeasureTheory.OuterMeasure (α i)<VAR>s : (i : ι) → Set (α i)<GOAL>(MeasureTheory.OuterMeasure.pi m) (Set.univ.pi s) ≤ ∏ i : ι, (m i) (s i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>m : (i : ι) → MeasureTheory.OuterMeasure (α i)<VAR>n : MeasureTheory.OuterMeasure ((i : ι) → α i)<GOAL>n ≤ MeasureTheory.OuterMeasure.pi m ↔ ∀ (s : (i : ι) → Set (α i)), (Set.univ.pi s).Nonempty → n (Set.univ.pi s) ≤ ∏ i : ι, (m i) (s i)
<VAR>δ : Type u_4<VAR>π : δ → Type u_5<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<GOAL>MeasureTheory.Measure.tprod [] μ = MeasureTheory.Measure.dirac PUnit.unit
<VAR>δ : Type u_4<VAR>π : δ → Type u_5<VAR>(x : δ) → MeasurableSpace (π x)<VAR>i : δ<VAR>l : List δ<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<GOAL>MeasureTheory.Measure.tprod (i :: l) μ = (μ i).prod (MeasureTheory.Measure.tprod l μ)
<VAR>δ : Type u_4<VAR>π : δ → Type u_5<VAR>(x : δ) → MeasurableSpace (π x)<VAR>l : List δ<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>∀ (i : δ), MeasureTheory.SigmaFinite (μ i)<VAR>s : (i : δ) → Set (π i)<GOAL>(MeasureTheory.Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i => (μ i) (s i)) l).prod
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>Encodable ι<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>s : (i : ι) → Set (α i)<GOAL>(MeasureTheory.Measure.pi' μ) (Set.univ.pi s) = ∏ i : ι, (μ i) (s i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<GOAL>MeasurableSpace.pi ≤ (MeasureTheory.OuterMeasure.pi fun i => (μ i).toOuterMeasure).caratheodory
<VAR>ι : Type u_4<VAR>α : ι → Type u_5<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<GOAL>MeasureTheory.Measure.pi μ = (MeasureTheory.OuterMeasure.pi fun i => (μ i).toOuterMeasure).toMeasure ⋯
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>s : (i : ι) → Set (α i)<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<GOAL>(MeasureTheory.Measure.pi μ) (Set.univ.pi s) = ∏ i : ι, (μ i) (s i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>C : (i : ι) → Set (Set (α i))<VAR>hC : ∀ (i : ι), MeasurableSpace.generateFrom (C i) = inst✝ i<VAR>h2C : ∀ (i : ι), IsPiSystem (C i)<VAR>h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)<VAR>μν : MeasureTheory.Measure ((i : ι) → α i)<VAR>h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → μν (Set.univ.pi s) = ∏ i : ι, (μ i) (s i)<GOAL>MeasureTheory.Measure.pi μ = μν
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>μ' : MeasureTheory.Measure ((i : ι) → α i)<VAR>h : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), MeasurableSet (s i)) → μ' (Set.univ.pi s) = ∏ i : ι, (μ i) (s i)<GOAL>MeasureTheory.Measure.pi μ = μ'
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>Encodable ι<GOAL>MeasureTheory.Measure.pi' μ = MeasureTheory.Measure.pi μ
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>s : (i : ι) → Set (α i)<GOAL>(MeasureTheory.Measure.pi μ) (Set.univ.pi s) = ∏ i : ι, (μ i) (s i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<GOAL>(MeasureTheory.Measure.pi μ) Set.univ = ∏ i : ι, (μ i) Set.univ
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>(i : ι) → MetricSpace (α i)<VAR>x : (i : ι) → α i<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(MeasureTheory.Measure.pi μ) (Metric.ball x r) = ∏ i : ι, (μ i) (Metric.ball (x i) r)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>(i : ι) → MetricSpace (α i)<VAR>x : (i : ι) → α i<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>(MeasureTheory.Measure.pi μ) (Metric.closedBall x r) = ∏ i : ι, (μ i) (Metric.closedBall (x i) r)
<VAR>α : Type u_4<VAR>Fintype α<VAR>IsEmpty α<VAR>β : α → Type u_5<VAR>m : (a : α) → MeasurableSpace (β a)<VAR>μ : (a : α) → MeasureTheory.Measure (β a)<VAR>x : (a : α) → β a := fun a => isEmptyElim a<GOAL>MeasureTheory.Measure.pi μ = MeasureTheory.Measure.dirac x
<VAR>ι : Type u_4<VAR>Fintype ι<VAR>IsEmpty ι<VAR>α : ι → Type u_5<VAR>(i : ι) → MeasureTheory.MeasureSpace (α i)<VAR>x : (a : ι) → α a := fun a => isEmptyElim a<GOAL>MeasureTheory.volume = MeasureTheory.Measure.dirac x
<VAR>α : Type u_4<VAR>Fintype α<VAR>IsEmpty α<VAR>β : α → Type u_5<VAR>m : (α : α) → MeasurableSpace (β α)<VAR>μ : (a : α) → MeasureTheory.Measure (β a)<GOAL>(MeasureTheory.Measure.pi μ) Set.univ = 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>i : ι<VAR>s : Set (α i)<VAR>hs : (μ i) s = 0<GOAL>(MeasureTheory.Measure.pi μ) (Function.eval i ⁻¹' s) = 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>i : ι<VAR>MeasureTheory.NoAtoms (μ i)<VAR>x : α i<GOAL>(MeasureTheory.Measure.pi μ) {f | f i = x} = 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>i : ι<VAR>MeasureTheory.NoAtoms (μ i)<VAR>x : α i<GOAL>∀ᵐ (y : (i : ι) → α i) ∂MeasureTheory.Measure.pi μ, y i ≠ x
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>i : ι<GOAL>Filter.Tendsto (Function.eval i) (MeasureTheory.ae (MeasureTheory.Measure.pi μ)) (MeasureTheory.ae (μ i))
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<GOAL>MeasureTheory.ae (MeasureTheory.Measure.pi μ) ≤ Filter.pi fun i => MeasureTheory.ae (μ i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>β : ι → Type u_4<VAR>f f' : (i : ι) → α i → β i<VAR>h : ∀ (i : ι), f i =ᵐ[μ i] f' i<GOAL>(fun x i => f i (x i)) =ᵐ[MeasureTheory.Measure.pi μ] fun x i => f' i (x i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>β : ι → Type u_4<VAR>(i : ι) → Preorder (β i)<VAR>f f' : (i : ι) → α i → β i<VAR>h : ∀ (i : ι), f i ≤ᵐ[μ i] f' i<GOAL>(fun x i => f i (x i)) ≤ᵐ[MeasureTheory.Measure.pi μ] fun x i => f' i (x i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>I : Set ι<VAR>s t : (i : ι) → Set (α i)<VAR>h : ∀ i ∈ I, s i ≤ᵐ[μ i] t i<GOAL>I.pi s ≤ᵐ[MeasureTheory.Measure.pi μ] I.pi t
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>I : Set ι<VAR>s t : (i : ι) → Set (α i)<VAR>h : ∀ i ∈ I, s i =ᵐ[μ i] t i<GOAL>I.pi s =ᵐ[MeasureTheory.Measure.pi μ] I.pi t
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>Fintype ι<VAR>hι' : Fintype ι'<VAR>e : ι ≃ ι'<VAR>β : ι' → Type u_4<VAR>(i : ι') → MeasurableSpace (β i)<VAR>μ : (i : ι') → MeasureTheory.Measure (β i)<VAR>∀ (i : ι'), MeasureTheory.SigmaFinite (μ i)<GOAL>MeasureTheory.Measure.map (⇑(MeasurableEquiv.piCongrLeft (fun i => β i) e)) (MeasureTheory.Measure.pi fun i => μ (e i)) = MeasureTheory.Measure.pi μ
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>β : Option ι → Type u_4<VAR>(i : Option ι) → MeasurableSpace (β i)<VAR>μ : (i : Option ι) → MeasureTheory.Measure (β i)<VAR>∀ (i : Option ι), MeasureTheory.SigmaFinite (μ i)<GOAL>MeasureTheory.Measure.map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((MeasureTheory.Measure.pi fun i => μ (some i)).prod (μ none)) = MeasureTheory.Measure.pi μ
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>(i : ι) → PartialOrder (α i)<VAR>∀ (i : ι), MeasureTheory.NoAtoms (μ i)<VAR>s : Set ι<VAR>f : (i : ι) → α i<GOAL>(s.pi fun i => Set.Iio (f i)) =ᵐ[MeasureTheory.Measure.pi μ] s.pi fun i => Set.Iic (f i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>(i : ι) → PartialOrder (α i)<VAR>∀ (i : ι), MeasureTheory.NoAtoms (μ i)<VAR>s : Set ι<VAR>f : (i : ι) → α i<GOAL>(s.pi fun i => Set.Ioi (f i)) =ᵐ[MeasureTheory.Measure.pi μ] s.pi fun i => Set.Ici (f i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>(i : ι) → PartialOrder (α i)<VAR>∀ (i : ι), MeasureTheory.NoAtoms (μ i)<VAR>f : (i : ι) → α i<GOAL>(Set.univ.pi fun i => Set.Iio (f i)) =ᵐ[MeasureTheory.Measure.pi μ] Set.Iic f
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>(i : ι) → PartialOrder (α i)<VAR>∀ (i : ι), MeasureTheory.NoAtoms (μ i)<VAR>f : (i : ι) → α i<GOAL>(Set.univ.pi fun i => Set.Ioi (f i)) =ᵐ[MeasureTheory.Measure.pi μ] Set.Ici f
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>(i : ι) → PartialOrder (α i)<VAR>∀ (i : ι), MeasureTheory.NoAtoms (μ i)<VAR>s : Set ι<VAR>f g : (i : ι) → α i<GOAL>(s.pi fun i => Set.Ioo (f i) (g i)) =ᵐ[MeasureTheory.Measure.pi μ] s.pi fun i => Set.Icc (f i) (g i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>(i : ι) → PartialOrder (α i)<VAR>∀ (i : ι), MeasureTheory.NoAtoms (μ i)<VAR>s : Set ι<VAR>f g : (i : ι) → α i<GOAL>(s.pi fun i => Set.Ioo (f i) (g i)) =ᵐ[MeasureTheory.Measure.pi μ] s.pi fun i => Set.Ioc (f i) (g i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>(i : ι) → PartialOrder (α i)<VAR>∀ (i : ι), MeasureTheory.NoAtoms (μ i)<VAR>f g : (i : ι) → α i<GOAL>(Set.univ.pi fun i => Set.Ioo (f i) (g i)) =ᵐ[MeasureTheory.Measure.pi μ] Set.Icc f g
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>(i : ι) → PartialOrder (α i)<VAR>∀ (i : ι), MeasureTheory.NoAtoms (μ i)<VAR>s : Set ι<VAR>f g : (i : ι) → α i<GOAL>(s.pi fun i => Set.Ioc (f i) (g i)) =ᵐ[MeasureTheory.Measure.pi μ] s.pi fun i => Set.Icc (f i) (g i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>(i : ι) → PartialOrder (α i)<VAR>∀ (i : ι), MeasureTheory.NoAtoms (μ i)<VAR>f g : (i : ι) → α i<GOAL>(Set.univ.pi fun i => Set.Ioc (f i) (g i)) =ᵐ[MeasureTheory.Measure.pi μ] Set.Icc f g
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>(i : ι) → PartialOrder (α i)<VAR>∀ (i : ι), MeasureTheory.NoAtoms (μ i)<VAR>s : Set ι<VAR>f g : (i : ι) → α i<GOAL>(s.pi fun i => Set.Ico (f i) (g i)) =ᵐ[MeasureTheory.Measure.pi μ] s.pi fun i => Set.Icc (f i) (g i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>(i : ι) → PartialOrder (α i)<VAR>∀ (i : ι), MeasureTheory.NoAtoms (μ i)<VAR>f g : (i : ι) → α i<GOAL>(Set.univ.pi fun i => Set.Ico (f i) (g i)) =ᵐ[MeasureTheory.Measure.pi μ] Set.Icc f g
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>i : ι<VAR>MeasureTheory.NoAtoms (μ i)<GOAL>MeasureTheory.NoAtoms (MeasureTheory.Measure.pi μ)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasureTheory.MeasureSpace (α i)<GOAL>MeasureTheory.volume = MeasureTheory.Measure.pi fun x => MeasureTheory.volume
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasureTheory.MeasureSpace (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume<VAR>s : (i : ι) → Set (α i)<GOAL>MeasureTheory.volume (Set.univ.pi s) = ∏ i : ι, MeasureTheory.volume (s i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasureTheory.MeasureSpace (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume<VAR>(i : ι) → MetricSpace (α i)<VAR>x : (i : ι) → α i<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>MeasureTheory.volume (Metric.ball x r) = ∏ i : ι, MeasureTheory.volume (Metric.ball (x i) r)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → MeasureTheory.MeasureSpace (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume<VAR>(i : ι) → MetricSpace (α i)<VAR>x : (i : ι) → α i<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>MeasureTheory.volume (Metric.closedBall x r) = ∏ i : ι, MeasureTheory.volume (Metric.closedBall (x i) r)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>p : ι → Prop<VAR>DecidablePred p<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piEquivPiSubtypeProd α p)) (MeasureTheory.Measure.pi μ) ((MeasureTheory.Measure.pi fun i => μ ↑i).prod (MeasureTheory.Measure.pi fun i => μ ↑i))
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>α : ι → Type u_4<VAR>(i : ι) → MeasureTheory.MeasureSpace (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume<VAR>p : ι → Prop<VAR>DecidablePred p<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piEquivPiSubtypeProd α p)) MeasureTheory.volume MeasureTheory.volume
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>Fintype ι'<VAR>f : ι' ≃ ι<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piCongrLeft α f)) (MeasureTheory.Measure.pi fun i' => μ (f i')) (MeasureTheory.Measure.pi μ)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>Fintype ι<VAR>Fintype ι'<VAR>α : ι → Type u_4<VAR>f : ι' ≃ ι<VAR>(i : ι) → MeasureTheory.MeasureSpace (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piCongrLeft α f)) MeasureTheory.volume MeasureTheory.volume
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>Fintype ι<VAR>Fintype ι'<VAR>π : ι ⊕ ι' → Type u_4<VAR>m : (i : ι ⊕ ι') → MeasurableSpace (π i)<VAR>μ : (i : ι ⊕ ι') → MeasureTheory.Measure (π i)<VAR>∀ (i : ι ⊕ ι'), MeasureTheory.SigmaFinite (μ i)<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.sumPiEquivProdPi π).symm) ((MeasureTheory.Measure.pi fun i => μ (Sum.inl i)).prod (MeasureTheory.Measure.pi fun i => μ (Sum.inr i))) (MeasureTheory.Measure.pi μ)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>Fintype ι<VAR>Fintype ι'<VAR>π : ι ⊕ ι' → Type u_4<VAR>(i : ι ⊕ ι') → MeasureTheory.MeasureSpace (π i)<VAR>∀ (i : ι ⊕ ι'), MeasureTheory.SigmaFinite MeasureTheory.volume<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.sumPiEquivProdPi π).symm) MeasureTheory.volume MeasureTheory.volume
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>Fintype ι<VAR>Fintype ι'<VAR>π : ι ⊕ ι' → Type u_4<VAR>_m : (i : ι ⊕ ι') → MeasurableSpace (π i)<VAR>μ : (i : ι ⊕ ι') → MeasureTheory.Measure (π i)<VAR>∀ (i : ι ⊕ ι'), MeasureTheory.SigmaFinite (μ i)<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.sumPiEquivProdPi π)) (MeasureTheory.Measure.pi μ) ((MeasureTheory.Measure.pi fun i => μ (Sum.inl i)).prod (MeasureTheory.Measure.pi fun i => μ (Sum.inr i)))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>Fintype ι<VAR>Fintype ι'<VAR>π : ι ⊕ ι' → Type u_4<VAR>(i : ι ⊕ ι') → MeasureTheory.MeasureSpace (π i)<VAR>∀ (i : ι ⊕ ι'), MeasureTheory.SigmaFinite MeasureTheory.volume<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.sumPiEquivProdPi π)) MeasureTheory.volume MeasureTheory.volume
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>m : (i : Fin (n + 1)) → MeasurableSpace (α i)<VAR>μ : (i : Fin (n + 1)) → MeasureTheory.Measure (α i)<VAR>∀ (i : Fin (n + 1)), MeasureTheory.SigmaFinite (μ i)<VAR>i : Fin (n + 1)<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove α i)) (MeasureTheory.Measure.pi μ) ((μ i).prod (MeasureTheory.Measure.pi fun j => μ (i.succAbove j)))
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>(i : Fin (n + 1)) → MeasureTheory.MeasureSpace (α i)<VAR>∀ (i : Fin (n + 1)), MeasureTheory.SigmaFinite MeasureTheory.volume<VAR>i : Fin (n + 1)<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove α i)) MeasureTheory.volume MeasureTheory.volume
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>π : ι → Type u_4<VAR>Unique ι<VAR>m : (i : ι) → MeasurableSpace (π i)<VAR>μ : (i : ι) → MeasureTheory.Measure (π i)<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piUnique π)) (MeasureTheory.Measure.pi μ) (μ default)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>π : ι → Type u_4<VAR>Unique ι<VAR>(i : ι) → MeasureTheory.MeasureSpace (π i)<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piUnique π)) MeasureTheory.volume MeasureTheory.volume
<VAR>β : Type u<VAR>_m : MeasurableSpace β<VAR>μ : MeasureTheory.Measure β<VAR>α : Type v<VAR>Unique α<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.funUnique α β)) (MeasureTheory.Measure.pi fun x => μ) μ
<VAR>α : Type u<VAR>β : Type v<VAR>Unique α<VAR>MeasureTheory.MeasureSpace β<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.funUnique α β)) MeasureTheory.volume MeasureTheory.volume
<VAR>α : Fin 2 → Type u<VAR>m : (i : Fin 2) → MeasurableSpace (α i)<VAR>μ : (i : Fin 2) → MeasureTheory.Measure (α i)<VAR>∀ (i : Fin 2), MeasureTheory.SigmaFinite (μ i)<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinTwo α)) (MeasureTheory.Measure.pi μ) ((μ 0).prod (μ 1))
<VAR>α : Fin 2 → Type u<VAR>(i : Fin 2) → MeasureTheory.MeasureSpace (α i)<VAR>∀ (i : Fin 2), MeasureTheory.SigmaFinite MeasureTheory.volume<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinTwo α)) MeasureTheory.volume MeasureTheory.volume
<VAR>α : Type u<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<GOAL>MeasureTheory.MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) (MeasureTheory.Measure.pi ![μ, ν]) (μ.prod ν)
<VAR>α : Type u<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>MeasureTheory.MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) (MeasureTheory.Measure.pi fun x => μ) (μ.prod μ)
<VAR>α : Type u<VAR>MeasureTheory.MeasureSpace α<VAR>MeasureTheory.SigmaFinite MeasureTheory.volume<GOAL>MeasureTheory.MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) MeasureTheory.volume MeasureTheory.volume
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>Fintype ι<VAR>IsEmpty ι<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit)) (MeasureTheory.Measure.pi μ) (MeasureTheory.Measure.dirac ())
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>Fintype ι<VAR>IsEmpty ι<VAR>(i : ι) → MeasureTheory.MeasureSpace (α i)<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit)) MeasureTheory.volume MeasureTheory.volume
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>DecidableEq ι<VAR>s t : Finset ι<VAR>h : Disjoint s t<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinsetUnion α h)) ((MeasureTheory.Measure.pi fun i => μ ↑i).prod (MeasureTheory.Measure.pi fun i => μ ↑i)) (MeasureTheory.Measure.pi fun i => μ ↑i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_4<VAR>DecidableEq ι<VAR>s t : Finset ι<VAR>h : Disjoint s t<VAR>(i : ι) → MeasureTheory.MeasureSpace (α i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume<GOAL>MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinsetUnion α h)) MeasureTheory.volume MeasureTheory.volume