ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>ms : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.OuterMeasure.boundedBy ⇑μ = μ.toOuterMeasure
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t u : Set α<VAR>hs : MeasurableSet s<VAR>h : μ t = μ u<VAR>htu : t ⊆ u<VAR>ht_ne_top : μ t ≠ ⊤<GOAL>μ (t ∩ s) = μ (u ∩ s)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : μ t ≠ ⊤<GOAL>μ (MeasureTheory.toMeasurable μ t ∩ s) = μ (t ∩ s)
<VAR>α : Type u_1<VAR>_m : MeasurableSpace α<GOAL>MeasureTheory.Measure.toOuterMeasure 0 = 0
<VAR>α : Type u_1<VAR>_m : MeasurableSpace α<GOAL>⇑0 = 0
<VAR>α : Type u_1<VAR>IsEmpty α<GOAL>∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α), μ s = 0
<VAR>α : Type u_1<VAR>IsEmpty α<VAR>_m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ = 0
<VAR>α : Type u_1<VAR>_m : MeasurableSpace α<VAR>μ₁ μ₂ : MeasureTheory.Measure α<GOAL>(μ₁ + μ₂).toOuterMeasure = μ₁.toOuterMeasure + μ₂.toOuterMeasure
<VAR>α : Type u_1<VAR>_m : MeasurableSpace α<VAR>μ₁ μ₂ : MeasureTheory.Measure α<GOAL>⇑(μ₁ + μ₂) = ⇑μ₁ + ⇑μ₂
<VAR>α : Type u_1<VAR>_m : MeasurableSpace α<VAR>μ₁ μ₂ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>(μ₁ + μ₂) s = μ₁ s + μ₂ s
<VAR>α : Type u_1<VAR>R : Type u_6<VAR>SMul R ENNReal<VAR>IsScalarTower R ENNReal ENNReal<VAR>_m : MeasurableSpace α<VAR>c : R<VAR>μ : MeasureTheory.Measure α<GOAL>(c • μ).toOuterMeasure = c • μ.toOuterMeasure
<VAR>α : Type u_1<VAR>R : Type u_6<VAR>SMul R ENNReal<VAR>IsScalarTower R ENNReal ENNReal<VAR>_m : MeasurableSpace α<VAR>c : R<VAR>μ : MeasureTheory.Measure α<GOAL>⇑(c • μ) = c • ⇑μ
<VAR>α : Type u_1<VAR>R : Type u_6<VAR>SMul R ENNReal<VAR>IsScalarTower R ENNReal ENNReal<VAR>_m : MeasurableSpace α<VAR>c : R<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>(c • μ) s = c • μ s
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>_m : MeasurableSpace α<VAR>I : Finset ι<VAR>μ : ι → MeasureTheory.Measure α<GOAL>⇑(∑ i ∈ I, μ i) = ∑ i ∈ I, ⇑(μ i)
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>I : Finset ι<VAR>μ : ι → MeasureTheory.Measure α<VAR>s : Set α<GOAL>(∑ i ∈ I, μ i) s = ∑ i ∈ I, (μ i) s
<VAR>α : Type u_1<VAR>_m : MeasurableSpace α<VAR>c : NNReal<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>(c • μ) s = ↑c * μ s
<VAR>α : Type u_1<VAR>_m : MeasurableSpace α<VAR>c : NNReal<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>c • μ s = ↑c * μ s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : α → Prop<VAR>c : ENNReal<VAR>hc : c ≠ 0<GOAL>(∀ᵐ (x : α) ∂c • μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>c : ENNReal<VAR>hc : c ≠ 0<GOAL>MeasureTheory.ae (c • μ) = MeasureTheory.ae μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : (μ + ν) t ≠ ⊤<VAR>h' : s ⊆ t<VAR>h'' : (μ + ν) s = (μ + ν) t<GOAL>μ s = μ t
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : (μ + ν) t ≠ ⊤<VAR>h' : s ⊆ t<VAR>h'' : (μ + ν) s = (μ + ν) t<GOAL>ν s = ν t
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : (μ + ν) t ≠ ⊤<GOAL>μ (MeasureTheory.toMeasurable (μ + ν) t ∩ s) = μ (t ∩ s)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : (μ + ν) t ≠ ⊤<GOAL>ν (MeasureTheory.toMeasurable (μ + ν) t ∩ s) = ν (t ∩ s)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ₁ μ₂ : MeasureTheory.Measure α<GOAL>μ₁.toOuterMeasure ≤ μ₂.toOuterMeasure ↔ μ₁ ≤ μ₂
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ₁ μ₂ : MeasureTheory.Measure α<GOAL>μ₁ ≤ μ₂ ↔ ∀ (s : Set α), MeasurableSet s → μ₁ s ≤ μ₂ s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ₁ μ₂ : MeasureTheory.Measure α<VAR>h : ∀ (s : Set α), MeasurableSet s → s.Nonempty → μ₁ s ≤ μ₂ s<GOAL>μ₁ ≤ μ₂
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ₁ μ₂ : MeasureTheory.Measure α<GOAL>μ₁ ≤ μ₂ ↔ ∀ (s : Set α), μ₁ s ≤ μ₂ s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>μ < ν ↔ μ ≤ ν ∧ ∃ s, MeasurableSet s ∧ μ s < ν s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>μ < ν ↔ μ ≤ ν ∧ ∃ s, μ s < ν s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν ν' : MeasureTheory.Measure α<VAR>h : μ ≤ ν<GOAL>μ ≤ ν' + ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν ν' : MeasureTheory.Measure α<VAR>h : μ ≤ ν<GOAL>μ ≤ ν + ν'
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>m : Set (MeasureTheory.Measure α)<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>s : Set α<VAR>m : Set (MeasureTheory.Measure α)<VAR>hs : MeasurableSet s<GOAL>(sInf m) s = (sInf (MeasureTheory.Measure.toOuterMeasure '' m)) s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>m : Set (MeasureTheory.Measure α)<VAR>h : μ ∈ m<GOAL>sInf m ≤ μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>m : Set (MeasureTheory.Measure α)<VAR>h : ∀ μ' ∈ m, μ ≤ μ'<GOAL>μ ≤ sInf m
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<GOAL>⊤.toMeasure ⋯ = ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>⊤.toOuterMeasure = ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>⊤ + μ = ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ + ⊤ = ⊤
<VAR>α : Type u_1<VAR>_m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>0 ≤ μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ ≤ 0 ↔ μ = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ Set.univ = 0 ↔ μ = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ Set.univ ≠ 0 ↔ μ ≠ 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>0 < μ Set.univ ↔ μ ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β<VAR>hf : ∀ (μ : MeasureTheory.Measure α), inst✝ ≤ (f μ.toOuterMeasure).caratheodory<VAR>s : Set β<VAR>hs : MeasureTheory.NullMeasurableSet s ((MeasureTheory.Measure.liftLinear f hf) μ)<GOAL>((MeasureTheory.Measure.liftLinear f hf) μ) s = (f μ.toOuterMeasure) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β<VAR>hf : ∀ (μ : MeasureTheory.Measure α), inst✝ ≤ (f μ.toOuterMeasure).caratheodory<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((MeasureTheory.Measure.liftLinear f hf) μ) s = (f μ.toOuterMeasure) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β<VAR>hf : ∀ (μ : MeasureTheory.Measure α), inst✝ ≤ (f μ.toOuterMeasure).caratheodory<VAR>s : Set β<GOAL>(f μ.toOuterMeasure) s ≤ ((MeasureTheory.Measure.liftLinear f hf) μ) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → β<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>h : f =ᵐ[μ] g<GOAL>(MeasureTheory.Measure.mapₗ f) μ = (MeasureTheory.Measure.mapₗ g) μ
<VAR>α : Type u_8<VAR>β : Type u_9<VAR>MeasurableSpace β<VAR>MeasurableSpace α<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.Measure.map f μ = if hf : AEMeasurable f μ then (MeasureTheory.Measure.mapₗ (AEMeasurable.mk f hf)) μ else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<GOAL>(MeasureTheory.Measure.mapₗ (AEMeasurable.mk f hf)) μ = MeasureTheory.Measure.map f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>hf : Measurable f<VAR>μ : MeasureTheory.Measure α<GOAL>(MeasureTheory.Measure.mapₗ f) μ = MeasureTheory.Measure.map f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ ν : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : Measurable f<GOAL>MeasureTheory.Measure.map f (μ + ν) = MeasureTheory.Measure.map f μ + MeasureTheory.Measure.map f ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<GOAL>MeasureTheory.Measure.map f 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>hf : ¬AEMeasurable f μ<GOAL>MeasureTheory.Measure.map f μ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → β<VAR>h : f =ᵐ[μ] g<GOAL>MeasureTheory.Measure.map f μ = MeasureTheory.Measure.map g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>c : ENNReal<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<GOAL>MeasureTheory.Measure.map f (c • μ) = c • MeasureTheory.Measure.map f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>c : NNReal<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<GOAL>MeasureTheory.Measure.map f (c • μ) = c • MeasureTheory.Measure.map f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>s : Set β<VAR>hs : MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.map f μ)<GOAL>(MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<GOAL>(MeasureTheory.Measure.map f μ).toOuterMeasure = ((MeasureTheory.OuterMeasure.map f) μ.toOuterMeasure).trim
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<GOAL>MeasureTheory.Measure.map f μ = 0 ↔ μ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : Measurable f<GOAL>(MeasureTheory.Measure.mapₗ f) μ = 0 ↔ μ = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → α<VAR>hf : MeasureTheory.Measure.map f μ = μ<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>μ (f ⁻¹' s) = μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<GOAL>MeasureTheory.Measure.map f μ ≠ 0 ↔ μ ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : Measurable f<GOAL>(MeasureTheory.Measure.mapₗ f) μ ≠ 0 ↔ μ ≠ 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.Measure.map id μ = μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.Measure.map (fun x => x) μ = μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>μ : MeasureTheory.Measure α<VAR>g : β → γ<VAR>f : α → β<VAR>hg : Measurable g<VAR>hf : Measurable f<GOAL>MeasureTheory.Measure.map g (MeasureTheory.Measure.map f μ) = MeasureTheory.Measure.map (g ∘ f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ ν : MeasureTheory.Measure α<VAR>f : α → β<VAR>h : μ ≤ ν<VAR>hf : Measurable f<GOAL>MeasureTheory.Measure.map f μ ≤ MeasureTheory.Measure.map f ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>s : Set β<GOAL>μ (f ⁻¹' s) ≤ (MeasureTheory.Measure.map f μ) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>s : Set α<GOAL>μ s ≤ (MeasureTheory.Measure.map f μ) (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>s : Set β<VAR>hs : (MeasureTheory.Measure.map f μ) s = 0<GOAL>μ (f ⁻¹' s) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<GOAL>Filter.Tendsto f (MeasureTheory.ae μ) (MeasureTheory.ae (MeasureTheory.Measure.map f μ))
<VAR>α : Type u_1<VAR>s : Set α<VAR>β : Type u_8<VAR>MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hfi : Function.Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)<VAR>μ : MeasureTheory.Measure β<VAR>hs : MeasurableSet s<GOAL>((MeasureTheory.Measure.comapₗ f) μ) s = μ (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>s : Set α<VAR>MeasurableSpace α<VAR>f : α → β<VAR>μ : MeasureTheory.Measure β<VAR>hfi : Function.Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ<VAR>hs : MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.comap f μ)<GOAL>(MeasureTheory.Measure.comap f μ) s = μ (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_8<VAR>MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure β<VAR>hfi : Function.Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ<VAR>s : Set α<GOAL>μ (f '' s) ≤ (MeasureTheory.Measure.comap f μ) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>β : Type u_8<VAR>MeasurableSpace α<VAR>_mβ : MeasurableSpace β<VAR>f : α → β<VAR>hfi : Function.Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)<VAR>μ : MeasureTheory.Measure β<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.Measure.comap f μ) s = μ (f '' s)
<VAR>α : Type u_1<VAR>s : Set α<VAR>β : Type u_8<VAR>MeasurableSpace α<VAR>_mβ : MeasurableSpace β<VAR>f : α → β<VAR>hfi : Function.Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)<VAR>μ : MeasureTheory.Measure β<VAR>hs : MeasurableSet s<GOAL>((MeasureTheory.Measure.comapₗ f) μ) s = (MeasureTheory.Measure.comap f μ) s
<VAR>α : Type u_1<VAR>β : Type u_8<VAR>MeasurableSpace α<VAR>_mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure β<VAR>hfi : Function.Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ<VAR>s : Set α<VAR>hs : (MeasureTheory.Measure.comap f μ) s = 0<GOAL>μ (f '' s) = 0
<VAR>α : Type u_1<VAR>β : Type u_8<VAR>MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure β<VAR>hfi : Function.Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ<VAR>s t : Set α<VAR>hst : s =ᵐ[MeasureTheory.Measure.comap f μ] t<GOAL>f '' s =ᵐ[μ] f '' t
<VAR>α : Type u_1<VAR>β : Type u_8<VAR>MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure β<VAR>hfi : Function.Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.comap f μ)<GOAL>MeasureTheory.NullMeasurableSet (f '' s) μ
<VAR>α : Type u_1<VAR>β : Type u_8<VAR>MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure β<VAR>s : Set β<VAR>hf : Function.Injective f<VAR>hf' : Measurable f<VAR>h : ∀ (t : Set α), MeasurableSet t → MeasureTheory.NullMeasurableSet (f '' t) μ<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.Measure.comap f μ) (f ⁻¹' s) = μ (s ∩ Set.range f)
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>f : ι → MeasureTheory.Measure α<VAR>s : Set α<GOAL>∑' (i : ι), (f i) s ≤ (MeasureTheory.Measure.sum f) s
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>f : ι → MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.Measure.sum f) s = ∑' (i : ι), (f i) s
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>f : ι → MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.sum f)<GOAL>(MeasureTheory.Measure.sum f) s = ∑' (i : ι), (f i) s
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>Countable ι<VAR>f : ι → MeasureTheory.Measure α<VAR>s : Set α<GOAL>(MeasureTheory.Measure.sum f) s = ∑' (i : ι), (f i) s
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>μ : ι → MeasureTheory.Measure α<VAR>i : ι<GOAL>μ i ≤ MeasureTheory.Measure.sum μ
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>Countable ι<VAR>μ : ι → MeasureTheory.Measure α<VAR>s : Set α<GOAL>(MeasureTheory.Measure.sum μ) s = 0 ↔ ∀ (i : ι), (μ i) s = 0
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>μ : ι → MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.Measure.sum μ) s = 0 ↔ ∀ (i : ι), (μ i) s = 0
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<GOAL>(MeasureTheory.Measure.sum fun x => 0) = 0
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>ι' : Type u_8<VAR>μ : ι → ι' → MeasureTheory.Measure α<GOAL>(MeasureTheory.Measure.sum fun n => MeasureTheory.Measure.sum (μ n)) = MeasureTheory.Measure.sum fun p => μ p.1 p.2
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>ι' : Type u_8<VAR>μ : ι → ι' → MeasureTheory.Measure α<GOAL>(MeasureTheory.Measure.sum fun n => MeasureTheory.Measure.sum (μ n)) = MeasureTheory.Measure.sum fun m => MeasureTheory.Measure.sum fun n => μ n m
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>Countable ι<VAR>μ : ι → MeasureTheory.Measure α<VAR>p : α → Prop<GOAL>(∀ᵐ (x : α) ∂MeasureTheory.Measure.sum μ, p x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ i, p x
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>μ : ι → MeasureTheory.Measure α<VAR>p : α → Prop<VAR>h : MeasurableSet {x | p x}<GOAL>(∀ᵐ (x : α) ∂MeasureTheory.Measure.sum μ, p x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ i, p x
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>Fintype ι<VAR>μ : ι → MeasureTheory.Measure α<GOAL>MeasureTheory.Measure.sum μ = ∑ i : ι, μ i
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>s : Finset ι<VAR>μ : ι → MeasureTheory.Measure α<GOAL>(MeasureTheory.Measure.sum fun i => μ ↑i) = ∑ i ∈ s, μ i
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>Countable ι<VAR>μ : ι → MeasureTheory.Measure α<GOAL>MeasureTheory.ae (MeasureTheory.Measure.sum μ) = ⨆ i, MeasureTheory.ae (μ i)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>f : Bool → MeasureTheory.Measure α<GOAL>MeasureTheory.Measure.sum f = f true + f false
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>(MeasureTheory.Measure.sum fun b => bif b then μ else ν) = μ + ν
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>IsEmpty ι<VAR>μ : ι → MeasureTheory.Measure α<GOAL>MeasureTheory.Measure.sum μ = 0
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>s : Set ι<VAR>μ : ι → MeasureTheory.Measure α<GOAL>((MeasureTheory.Measure.sum fun i => μ ↑i) + MeasureTheory.Measure.sum fun i => μ ↑i) = MeasureTheory.Measure.sum μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : ℕ → MeasureTheory.Measure α<VAR>h : ∀ (n : ℕ), μ n = ν n<GOAL>MeasureTheory.Measure.sum μ = MeasureTheory.Measure.sum ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>ι : Type u_8<VAR>μ ν : ι → MeasureTheory.Measure α<GOAL>MeasureTheory.Measure.sum μ + MeasureTheory.Measure.sum ν = MeasureTheory.Measure.sum fun n => μ n + ν n
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>e : ι' ≃ ι<VAR>m : ι → MeasureTheory.Measure α<GOAL>MeasureTheory.Measure.sum (m ∘ ⇑e) = MeasureTheory.Measure.sum m
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>f : ι → ι'<VAR>hf : Function.Injective f<VAR>m : ι → MeasureTheory.Measure α<GOAL>MeasureTheory.Measure.sum (Function.extend f m 0) = MeasureTheory.Measure.sum m
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : μ ≤ ν<GOAL>μ.AbsolutelyContinuous ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : μ = ν<GOAL>μ.AbsolutelyContinuous ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0<GOAL>μ.AbsolutelyContinuous ν
<VAR>α : Type u_1<VAR>_m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ.AbsolutelyContinuous μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ.AbsolutelyContinuous μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.Measure.AbsolutelyContinuous 0 μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ₁ μ₂ μ₃ : MeasureTheory.Measure α<VAR>h1 : μ₁.AbsolutelyContinuous μ₂<VAR>h2 : μ₂.AbsolutelyContinuous μ₃<GOAL>μ₁.AbsolutelyContinuous μ₃
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ ν : MeasureTheory.Measure α<VAR>h : μ.AbsolutelyContinuous ν<VAR>f : α → β<VAR>hf : Measurable f<GOAL>(MeasureTheory.Measure.map f μ).AbsolutelyContinuous (MeasureTheory.Measure.map f ν)
<VAR>α : Type u_1<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>Monoid R<VAR>DistribMulAction R ENNReal<VAR>IsScalarTower R ENNReal ENNReal<VAR>h : μ.AbsolutelyContinuous ν<VAR>c : R<GOAL>(c • μ).AbsolutelyContinuous ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ₁ μ₂ ν ν' : MeasureTheory.Measure α<VAR>h1 : μ₁.AbsolutelyContinuous ν<VAR>h2 : μ₂.AbsolutelyContinuous ν'<GOAL>(μ₁ + μ₂).AbsolutelyContinuous (ν + ν')
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ₁ μ₂ ν : MeasureTheory.Measure α<GOAL>(μ₁ + μ₂).AbsolutelyContinuous ν ↔ μ₁.AbsolutelyContinuous ν ∧ μ₂.AbsolutelyContinuous ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ₁ μ₂ ν : MeasureTheory.Measure α<VAR>h₁ : μ₁.AbsolutelyContinuous ν<VAR>h₂ : μ₂.AbsolutelyContinuous ν<GOAL>(μ₁ + μ₂).AbsolutelyContinuous ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h1 : μ.AbsolutelyContinuous ν<VAR>ν' : MeasureTheory.Measure α<GOAL>μ.AbsolutelyContinuous (ν + ν')
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ.AbsolutelyContinuous 0 ↔ μ = 0
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>μs : ι → MeasureTheory.Measure α<VAR>hμs : ∀ (i : ι), (μs i).AbsolutelyContinuous ν<GOAL>(MeasureTheory.Measure.sum μs).AbsolutelyContinuous ν
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m0 : MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>μs : ι → MeasureTheory.Measure α<VAR>i : ι<VAR>hνμ : ν.AbsolutelyContinuous (μs i)<GOAL>ν.AbsolutelyContinuous (MeasureTheory.Measure.sum μs)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ μ' : MeasureTheory.Measure α<VAR>c : ENNReal<VAR>hμ'_le : μ' ≤ c • μ<GOAL>μ'.AbsolutelyContinuous μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>c : ENNReal<GOAL>(c • μ).AbsolutelyContinuous μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>c : ENNReal<VAR>hc : c ≠ 0<GOAL>μ.AbsolutelyContinuous (c • μ)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>MeasureTheory.ae μ ≤ MeasureTheory.ae ν ↔ μ.AbsolutelyContinuous ν