ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>ab : α ≃ᵐ β<VAR>bc : β ≃ᵐ γ<GOAL>⇑(ab.trans bc) = ⇑bc ∘ ⇑ab
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<GOAL>⇑e.symm = ⇑e.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e₁ e₂ : α ≃ᵐ β<VAR>h : ⇑e₁ = ⇑e₂<GOAL>e₁ = e₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ β<VAR>h1 : Measurable ⇑e<VAR>h2 : Measurable ⇑e.symm<GOAL>{ toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 }.symm = { toEquiv := e.symm, measurable_toFun := h2, measurable_invFun := h1 }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<GOAL>e.symm.symm = e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<GOAL>Function.Bijective MeasurableEquiv.symm
<VAR>α : Type u_6<VAR>MeasurableSpace α<GOAL>(MeasurableEquiv.refl α).symm = MeasurableEquiv.refl α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<GOAL>⇑e.symm ∘ ⇑e = id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<GOAL>⇑e ∘ ⇑e.symm = id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<VAR>y : β<GOAL>e (e.symm y) = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<VAR>x : α<GOAL>e.symm (e x) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<GOAL>e.symm.trans e = MeasurableEquiv.refl β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<GOAL>e.trans e.symm = MeasurableEquiv.refl α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<GOAL>Function.Surjective ⇑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<GOAL>Function.Bijective ⇑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<GOAL>Function.Injective ⇑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<VAR>s : Set β<GOAL>⇑e.symm ⁻¹' (⇑e ⁻¹' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<VAR>s : Set α<GOAL>⇑e '' s = ⇑e.symm ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<VAR>s : Set α<GOAL>⇑e.symm ⁻¹' s = ⇑e '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<VAR>s : Set β<GOAL>⇑e.symm '' s = ⇑e ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<VAR>s : Set β<VAR>t : Set α<GOAL>s = ⇑e '' t ↔ ⇑e.symm '' s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<VAR>s : Set β<GOAL>⇑e '' (⇑e ⁻¹' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<VAR>s : Set α<GOAL>⇑e ⁻¹' (⇑e '' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<VAR>s : Set β<GOAL>MeasurableSet (⇑e ⁻¹' s) ↔ MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<GOAL>MeasurableSet (⇑e '' s) ↔ MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<GOAL>MeasurableSpace.map (⇑e) inst✝ = inst✝¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<GOAL>MeasurableEmbedding ⇑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>f : β → γ<VAR>e : α ≃ᵐ β<GOAL>Measurable (f ∘ ⇑e) ↔ Measurable f
<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>π : δ' → Type u_6<VAR>(x : δ') → MeasurableSpace (π x)<VAR>f : δ ≃ δ'<GOAL>⇑(MeasurableEquiv.piCongrLeft π f) = ⇑(Equiv.piCongrLeft π f)
<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>e : ι ≃ ι'<VAR>β : ι' → Type u_10<VAR>(i' : ι') → MeasurableSpace (β i')<VAR>x : (i : ι) → β (e i)<VAR>i : ι<GOAL>(MeasurableEquiv.piCongrLeft (fun i' => β i') e) x (e i) = x i
<VAR>δ' : Type u_5<VAR>π : δ' → Type u_6<VAR>(x : δ') → MeasurableSpace (π x)<VAR>DecidableEq δ'<VAR>l : List δ'<VAR>hnd : l.Nodup<VAR>h : ∀ (i : δ'), i ∈ l<GOAL>⇑(MeasurableEquiv.piMeasurableEquivTProd hnd h) = List.TProd.mk l
<VAR>δ' : Type u_5<VAR>π : δ' → Type u_6<VAR>(x : δ') → MeasurableSpace (π x)<VAR>DecidableEq δ'<VAR>l : List δ'<VAR>hnd : l.Nodup<VAR>h : ∀ (i : δ'), i ∈ l<GOAL>⇑(MeasurableEquiv.piMeasurableEquivTProd hnd h).symm = List.TProd.elim' h
<VAR>δ' : Type u_5<VAR>π : δ' → Type u_6<VAR>(x : δ') → MeasurableSpace (π x)<VAR>Unique δ'<GOAL>⇑(MeasurableEquiv.piUnique π).symm = uniqueElim
<VAR>δ' : Type u_5<VAR>π : δ' → Type u_6<VAR>(x : δ') → MeasurableSpace (π x)<VAR>Unique δ'<GOAL>⇑(MeasurableEquiv.piUnique π) = fun f => f default
<VAR>α : Type u_8<VAR>β : Type u_9<VAR>Unique α<VAR>MeasurableSpace β<GOAL>⇑(MeasurableEquiv.funUnique α β).symm = uniqueElim
<VAR>α : Type u_8<VAR>β : Type u_9<VAR>Unique α<VAR>MeasurableSpace β<GOAL>⇑(MeasurableEquiv.funUnique α β) = fun f => f default
<VAR>α : Fin 2 → Type u_8<VAR>(i : Fin 2) → MeasurableSpace (α i)<GOAL>⇑(MeasurableEquiv.piFinTwo α).symm = fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
<VAR>α : Fin 2 → Type u_8<VAR>(i : Fin 2) → MeasurableSpace (α i)<GOAL>⇑(MeasurableEquiv.piFinTwo α) = fun f => (f 0, f 1)
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>⇑MeasurableEquiv.finTwoArrow = fun f => (f 0, f 1)
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>⇑MeasurableEquiv.finTwoArrow.symm = fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_8<VAR>(i : Fin (n + 1)) → MeasurableSpace (α i)<VAR>i : Fin (n + 1)<GOAL>⇑(MeasurableEquiv.piFinSuccAbove α i).symm = fun f => i.insertNth f.1 f.2
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_8<VAR>(i : Fin (n + 1)) → MeasurableSpace (α i)<VAR>i : Fin (n + 1)<GOAL>⇑(MeasurableEquiv.piFinSuccAbove α i) = fun f => (f i, i.removeNth f)
<VAR>δ' : Type u_5<VAR>π : δ' → Type u_6<VAR>(x : δ') → MeasurableSpace (π x)<VAR>p : δ' → Prop<VAR>DecidablePred p<GOAL>⇑(MeasurableEquiv.piEquivPiSubtypeProd π p) = fun f => (fun x => f ↑x, fun x => f ↑x)
<VAR>δ' : Type u_5<VAR>π : δ' → Type u_6<VAR>(x : δ') → MeasurableSpace (π x)<VAR>p : δ' → Prop<VAR>DecidablePred p<GOAL>⇑(MeasurableEquiv.piEquivPiSubtypeProd π p).symm = fun f x => if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩
<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>α : δ ⊕ δ' → Type u_8<VAR>(i : δ ⊕ δ') → MeasurableSpace (α i)<GOAL>⇑(MeasurableEquiv.sumPiEquivProdPi α) = ⇑(Equiv.sumPiEquivProdPi α)
<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>α : δ ⊕ δ' → Type u_8<VAR>(i : δ ⊕ δ') → MeasurableSpace (α i)<GOAL>⇑(MeasurableEquiv.sumPiEquivProdPi α).symm = ⇑(Equiv.sumPiEquivProdPi α).symm
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → α<VAR>hf : Function.Involutive f<VAR>hf' : Measurable f<GOAL>(MeasurableEquiv.ofInvolutive f hf hf').toEquiv = Function.Involutive.toPerm f hf
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → α<VAR>hf : Function.Involutive f<VAR>hf' : Measurable f<VAR>a : α<GOAL>(MeasurableEquiv.ofInvolutive f hf hf') a = f a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → α<VAR>hf : Function.Involutive f<VAR>hf' : Measurable f<GOAL>(MeasurableEquiv.ofInvolutive f hf hf').symm = MeasurableEquiv.ofInvolutive f hf hf'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<GOAL>MeasurableSpace.comap f inst✝ = inst✝¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<GOAL>MeasurableEmbedding f ↔ Function.Injective f ∧ MeasurableSpace.comap f inst✝ = inst✝¹ ∧ MeasurableSet (Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>g : ↑(Set.range f) → α<VAR>hf₁ : Measurable f<VAR>hf₂ : MeasurableSet (Set.range f)<VAR>hg : Measurable g<VAR>H : Function.LeftInverse g (Set.rangeFactorization f)<GOAL>MeasurableEmbedding f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>g : β → α<VAR>hf₁ : Measurable f<VAR>hf₂ : MeasurableSet (Set.range f)<VAR>hg : Measurable g<VAR>H : Function.LeftInverse g f<GOAL>MeasurableEmbedding f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m' : MeasurableSpace β<VAR>BooleanAlgebra β<VAR>h : Measurable compl<VAR>f : α → β<GOAL>MeasurableSpace.comap (fun a => (f a)ᶜ) inferInstance = MeasurableSpace.comap f inferInstance
<VAR>α : Type u_1<VAR>p : α → Prop<GOAL>MeasurableSpace.comap (fun a => ¬p a) inferInstance = MeasurableSpace.comap p inferInstance
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : X → E<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x = g x<GOAL>∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : X → E<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>hs : MeasurableSet s<VAR>h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x = g x<GOAL>∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : X → E<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>h : Set.EqOn f g s<GOAL>∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : X → E<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>hs : MeasurableSet s<VAR>h : Set.EqOn f g s<GOAL>∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>hst : s =ᵐ[μ] t<GOAL>∫ (x : X) in s, f x ∂μ = ∫ (x : X) in t, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>hst : MeasureTheory.AEDisjoint μ s t<VAR>ht : MeasureTheory.NullMeasurableSet t μ<VAR>hfs : MeasureTheory.IntegrableOn f s μ<VAR>hft : MeasureTheory.IntegrableOn f t μ<GOAL>∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in t, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>hst : Disjoint s t<VAR>ht : MeasurableSet t<VAR>hfs : MeasureTheory.IntegrableOn f s μ<VAR>hft : MeasureTheory.IntegrableOn f t μ<GOAL>∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in t, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>ht : MeasurableSet t<VAR>hfs : MeasureTheory.IntegrableOn f s μ<VAR>hts : t ⊆ s<GOAL>∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ - ∫ (x : X) in t, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>ht : MeasureTheory.NullMeasurableSet t μ<VAR>hfs : MeasureTheory.IntegrableOn f s μ<GOAL>∫ (x : X) in s ∩ t, f x ∂μ + ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>ht : MeasurableSet t<VAR>hfs : MeasureTheory.IntegrableOn f s μ<GOAL>∫ (x : X) in s ∩ t, f x ∂μ + ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>ι : Type u_5<VAR>t : Finset ι<VAR>s : ι → Set X<VAR>hs : ∀ i ∈ t, MeasurableSet (s i)<VAR>h's : (↑t).Pairwise (Disjoint on s)<VAR>hf : ∀ i ∈ t, MeasureTheory.IntegrableOn f (s i) μ<GOAL>∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>ι : Type u_5<VAR>Fintype ι<VAR>s : ι → Set X<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>h's : Pairwise (Disjoint on s)<VAR>hf : ∀ (i : ι), MeasureTheory.IntegrableOn f (s i) μ<GOAL>∫ (x : X) in ⋃ i, s i, f x ∂μ = ∑ i : ι, ∫ (x : X) in s i, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<GOAL>∫ (x : X) in ∅, f x ∂μ = 0
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<GOAL>∫ (x : X) in Set.univ, f x ∂μ = ∫ (x : X), f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>∫ (x : X) in s, f x ∂μ + ∫ (x : X) in sᶜ, f x ∂μ = ∫ (x : X), f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>hs : MeasurableSet s<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>∫ (x : X) in s, f x ∂μ + ∫ (x : X) in sᶜ, f x ∂μ = ∫ (x : X), f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>hs : MeasurableSet s<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>∫ (x : X) in sᶜ, f x ∂μ = ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>hs : MeasurableSet s<GOAL>∫ (x : X), s.indicator f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>ht : MeasurableSet t<GOAL>∫ (x : X) in s, t.indicator f x ∂μ = ∫ (x : X) in s ∩ t, f x ∂μ
<VAR>X : Type u_5<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>hs : μ s ≠ ⊤<GOAL>ENNReal.ofReal (∫ (x : X) in s, 1 ∂μ) = μ s
<VAR>X : Type u_5<GOAL>∀ {x : MeasurableSpace X} (μ : MeasureTheory.Measure X) [inst : MeasureTheory.IsFiniteMeasure μ] (s : Set X), ENNReal.ofReal (∫ (x : X) in s, 1 ∂μ) = μ s
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : X → E<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<VAR>hf : MeasureTheory.IntegrableOn f s μ<VAR>hg : MeasureTheory.IntegrableOn g sᶜ μ<GOAL>∫ (x : X), s.piecewise f g x ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in sᶜ, g x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>ι : Type u_5<VAR>Countable ι<VAR>SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_mono : Monotone s<VAR>hfi : MeasureTheory.IntegrableOn f (⋃ n, s n) μ<GOAL>Filter.Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) Filter.atTop (𝓝 (∫ (x : X) in ⋃ n, s n, f x ∂μ))
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>ι : Type u_5<VAR>Countable ι<VAR>SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>hfi : ∃ i, MeasureTheory.IntegrableOn f (s i) μ<GOAL>Filter.Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) Filter.atTop (𝓝 (∫ (x : X) in ⋂ n, s n, f x ∂μ))
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>ι : Type u_5<VAR>Countable ι<VAR>s : ι → Set X<VAR>hm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ<VAR>hd : Pairwise (MeasureTheory.AEDisjoint μ on s)<VAR>hfi : MeasureTheory.IntegrableOn f (⋃ i, s i) μ<GOAL>HasSum (fun n => ∫ (x : X) in s n, f x ∂μ) (∫ (x : X) in ⋃ n, s n, f x ∂μ)
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>ι : Type u_5<VAR>Countable ι<VAR>s : ι → Set X<VAR>hm : ∀ (i : ι), MeasurableSet (s i)<VAR>hd : Pairwise (Disjoint on s)<VAR>hfi : MeasureTheory.IntegrableOn f (⋃ i, s i) μ<GOAL>HasSum (fun n => ∫ (x : X) in s n, f x ∂μ) (∫ (x : X) in ⋃ n, s n, f x ∂μ)
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>ι : Type u_5<VAR>Countable ι<VAR>s : ι → Set X<VAR>hm : ∀ (i : ι), MeasurableSet (s i)<VAR>hd : Pairwise (Disjoint on s)<VAR>hfi : MeasureTheory.IntegrableOn f (⋃ i, s i) μ<GOAL>∫ (x : X) in ⋃ n, s n, f x ∂μ = ∑' (n : ι), ∫ (x : X) in s n, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>ι : Type u_5<VAR>Countable ι<VAR>s : ι → Set X<VAR>hm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ<VAR>hd : Pairwise (MeasureTheory.AEDisjoint μ on s)<VAR>hfi : MeasureTheory.IntegrableOn f (⋃ i, s i) μ<GOAL>∫ (x : X) in ⋃ n, s n, f x ∂μ = ∑' (n : ι), ∫ (x : X) in s n, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0<GOAL>∫ (x : X) in t, f x ∂μ = 0
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>ht_eq : ∀ x ∈ t, f x = 0<GOAL>∫ (x : X) in t, f x ∂μ = 0
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0<VAR>haux : MeasureTheory.StronglyMeasurable f<VAR>H : MeasureTheory.IntegrableOn f (s ∪ t) μ<GOAL>∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0<GOAL>∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → E<VAR>ht : MeasureTheory.NullMeasurableSet t μ<VAR>ht_eq : ∀ x ∈ t, f x = 0<GOAL>∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → E<VAR>ht : MeasurableSet t<VAR>ht_eq : ∀ x ∈ t, f x = 0<GOAL>∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>hts : s ⊆ t<VAR>h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0<VAR>haux : MeasureTheory.StronglyMeasurable f<VAR>h'aux : MeasureTheory.IntegrableOn f t μ<GOAL>∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>ht : MeasureTheory.NullMeasurableSet t μ<VAR>hts : s ⊆ t<VAR>h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0<GOAL>∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>ht : MeasurableSet t<VAR>hts : s ⊆ t<VAR>h't : ∀ x ∈ t \ s, f x = 0<GOAL>∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0<GOAL>∫ (x : X) in s, f x ∂μ = ∫ (x : X), f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>h : ∀ x ∉ s, f x = 0<GOAL>∫ (x : X) in s, f x ∂μ = ∫ (x : X), f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure X<VAR>LinearOrder E<VAR>f : X → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>∫ (x : X) in {x | f x < 0}, f x ∂μ = ∫ (x : X) in {x | f x ≤ 0}, f x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>∫ (x : X), ‖f x‖ ∂μ = ∫ (x : X) in {x | 0 ≤ f x}, f x ∂μ - ∫ (x : X) in {x | f x ≤ 0}, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>CompleteSpace E<VAR>c : E<GOAL>∫ (x : X) in s, c ∂μ = (μ s).toReal • c
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure X<VAR>CompleteSpace E<VAR>e : E<VAR>s : Set X<VAR>s_meas : MeasurableSet s<GOAL>∫ (x : X), s.indicator (fun x => e) x ∂μ = (μ s).toReal • e
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>hs : MeasurableSet s<GOAL>∫ (x : X), s.indicator 1 x ∂μ = (μ s).toReal
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>CompleteSpace E<VAR>p : ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>e : E<GOAL>∫ (x : X) in s, ↑↑(MeasureTheory.indicatorConstLp p ht hμt e) x ∂μ = (μ (t ∩ s)).toReal • e
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>t : Set X<VAR>μ : MeasureTheory.Measure X<VAR>CompleteSpace E<VAR>p : ℝ≥0∞<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>e : E<GOAL>∫ (x : X), ↑↑(MeasureTheory.indicatorConstLp p ht hμt e) x ∂μ = (μ t).toReal • e
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure X<VAR>Y : Type u_5<VAR>MeasurableSpace Y<VAR>g : X → Y<VAR>f : Y → E<VAR>s : Set Y<VAR>hs : MeasurableSet s<VAR>hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map g μ)<VAR>hg : AEMeasurable g μ<GOAL>∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure X<VAR>Y : Type u_5<GOAL>∀ {x : MeasurableSpace Y} {f : X → Y}, MeasurableEmbedding f → ∀ (g : Y → E) (s : Set Y), ∫ (y : Y) in s, g y ∂MeasureTheory.Measure.map f μ = ∫ (x : X) in f ⁻¹' s, g (f x) ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure X<VAR>TopologicalSpace X<VAR>BorelSpace X<VAR>Y : Type u_5<VAR>MeasurableSpace Y<VAR>TopologicalSpace Y<VAR>BorelSpace Y<VAR>g : X → Y<VAR>f : Y → E<VAR>s : Set Y<VAR>hg : ClosedEmbedding g<GOAL>∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure X<VAR>Y : Type u_5<GOAL>∀ {x : MeasurableSpace Y} {f : X → Y} {ν : MeasureTheory.Measure Y}, MeasureTheory.MeasurePreserving f μ ν → MeasurableEmbedding f → ∀ (g : Y → E) (s : Set Y), ∫ (x : X) in f ⁻¹' s, g (f x) ∂μ = ∫ (y : Y) in s, g y ∂ν