ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → β<VAR>TopologicalSpace β<VAR>AddGroup β<VAR>ContinuousSub β<VAR>hf : MeasureTheory.FinStronglyMeasurable f μ<VAR>hg : MeasureTheory.FinStronglyMeasurable g μ<GOAL>MeasureTheory.FinStronglyMeasurable (f - g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>TopologicalSpace β<VAR>𝕜 : Type u_5<VAR>TopologicalSpace 𝕜<VAR>AddMonoid β<VAR>Monoid 𝕜<VAR>DistribMulAction 𝕜 β<VAR>ContinuousSMul 𝕜 β<VAR>hf : MeasureTheory.FinStronglyMeasurable f μ<VAR>c : 𝕜<GOAL>MeasureTheory.FinStronglyMeasurable (c • f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → β<VAR>TopologicalSpace β<VAR>Zero β<VAR>SemilatticeSup β<VAR>ContinuousSup β<VAR>hf : MeasureTheory.FinStronglyMeasurable f μ<VAR>hg : MeasureTheory.FinStronglyMeasurable g μ<GOAL>MeasureTheory.FinStronglyMeasurable (f ⊔ g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → β<VAR>TopologicalSpace β<VAR>Zero β<VAR>SemilatticeInf β<VAR>ContinuousInf β<VAR>hf : MeasureTheory.FinStronglyMeasurable f μ<VAR>hg : MeasureTheory.FinStronglyMeasurable g μ<GOAL>MeasureTheory.FinStronglyMeasurable (f ⊓ g) μ
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>f : α → β<VAR>TopologicalSpace β<VAR>T2Space β<VAR>Zero β<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α}, MeasureTheory.FinStronglyMeasurable f μ ↔ MeasureTheory.StronglyMeasurable f ∧ ∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ MeasureTheory.SigmaFinite (μ.restrict t)
<VAR>α : Type u_5<VAR>β : Type u_6<GOAL>∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : Zero β] [inst_1 : TopologicalSpace β], MeasureTheory.AEFinStronglyMeasurable 0 μ
<VAR>α : Type u_5<VAR>β : Type u_6<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β] {b : β}, MeasureTheory.AEStronglyMeasurable (fun x => b) μ
<VAR>α : Type u_5<VAR>β : Type u_6<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β] [inst_1 : Zero β], MeasureTheory.AEStronglyMeasurable 0 μ
<VAR>α : Type u_5<VAR>β : Type u_6<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β] [inst_1 : One β], MeasureTheory.AEStronglyMeasurable 1 μ
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Subsingleton β] {μ : MeasureTheory.Measure α} (f : α → β), MeasureTheory.AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Subsingleton α] {μ : MeasureTheory.Measure α} (f : α → β), MeasureTheory.AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>f : α → β<GOAL>MeasureTheory.AEStronglyMeasurable f 0
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β] (f : MeasureTheory.SimpleFunc α β), MeasureTheory.AEStronglyMeasurable (↑f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.StronglyMeasurable (MeasureTheory.AEStronglyMeasurable.mk f hf)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>Measurable (MeasureTheory.AEStronglyMeasurable.mk f hf)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>f =ᵐ[μ] MeasureTheory.AEStronglyMeasurable.mk f hf
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>BorelSpace β<VAR>f : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>h : f =ᵐ[μ] g<GOAL>MeasureTheory.AEStronglyMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>h : f =ᵐ[μ] g<GOAL>MeasureTheory.AEStronglyMeasurable f μ ↔ MeasureTheory.AEStronglyMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>ν : MeasureTheory.Measure α<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>h : ν ≤ μ<GOAL>MeasureTheory.AEStronglyMeasurable f ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>h : ν ≪ μ<VAR>hμ : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable f ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>ht : MeasureTheory.AEStronglyMeasurable f (μ.restrict t)<GOAL>MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hfm : MeasureTheory.AEStronglyMeasurable f μ<VAR>s : Set α<GOAL>MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>h : MeasureTheory.AEStronglyMeasurable f (μ.restrict s)<GOAL>∀ᵐ (x : α) ∂μ, x ∈ s → f x = MeasureTheory.AEStronglyMeasurable.mk f h x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : Continuous g<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => g (f x)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>SecondCountableTopologyEither α β<VAR>hf : Continuous f<GOAL>MeasureTheory.AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α → β<VAR>g : α → γ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => (f x, g x)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>β' : Type u_5<VAR>TopologicalSpace β'<VAR>g : β → β' → γ<VAR>f : α → β<VAR>f' : α → β'<VAR>hg : Continuous (Function.uncurry g)<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>h'f : MeasureTheory.AEStronglyMeasurable f' μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => g (f x) (f' x)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>f : α → β<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasurableSpace β] [inst_1 : TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : SecondCountableTopology β] [inst_3 : OpensMeasurableSpace β], Measurable f → MeasureTheory.AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>Mul β<VAR>ContinuousMul β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEStronglyMeasurable (f * g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>Add β<VAR>ContinuousAdd β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEStronglyMeasurable (f + g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>Add β<VAR>ContinuousAdd β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>c : β<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => f x + c) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>Mul β<VAR>ContinuousMul β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>c : β<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => f x * c) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>Add β<VAR>ContinuousAdd β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>c : β<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => c + f x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>Mul β<VAR>ContinuousMul β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>c : β<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => c * f x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>Inv β<VAR>ContinuousInv β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable f⁻¹ μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>Neg β<VAR>ContinuousNeg β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (-f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEStronglyMeasurable (f - g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>Group β<VAR>TopologicalGroup β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEStronglyMeasurable (f / g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>CommGroup β<VAR>TopologicalGroup β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (f * g) μ ↔ MeasureTheory.AEStronglyMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>AddCommGroup β<VAR>TopologicalAddGroup β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (f + g) μ ↔ MeasureTheory.AEStronglyMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>CommGroup β<VAR>TopologicalGroup β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (g * f) μ ↔ MeasureTheory.AEStronglyMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>AddCommGroup β<VAR>TopologicalAddGroup β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (g + f) μ ↔ MeasureTheory.AEStronglyMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>𝕜 : Type u_5<VAR>TopologicalSpace 𝕜<VAR>SMul 𝕜 β<VAR>ContinuousSMul 𝕜 β<VAR>f : α → 𝕜<VAR>g : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => f x • g x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>𝕜 : Type u_5<VAR>TopologicalSpace 𝕜<VAR>VAdd 𝕜 β<VAR>ContinuousVAdd 𝕜 β<VAR>f : α → 𝕜<VAR>g : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => f x +ᵥ g x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>Monoid β<VAR>ContinuousMul β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>n : ℕ<GOAL>MeasureTheory.AEStronglyMeasurable (f ^ n) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>AddMonoid β<VAR>ContinuousAdd β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>n : ℕ<GOAL>MeasureTheory.AEStronglyMeasurable (n • f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>𝕜 : Type u_5<VAR>VAdd 𝕜 β<VAR>ContinuousConstVAdd 𝕜 β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>c : 𝕜<GOAL>MeasureTheory.AEStronglyMeasurable (c +ᵥ f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>𝕜 : Type u_5<VAR>SMul 𝕜 β<VAR>ContinuousConstSMul 𝕜 β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>c : 𝕜<GOAL>MeasureTheory.AEStronglyMeasurable (c • f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>𝕜 : Type u_5<VAR>VAdd 𝕜 β<VAR>ContinuousConstVAdd 𝕜 β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>c : 𝕜<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => c +ᵥ f x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>𝕜 : Type u_5<VAR>SMul 𝕜 β<VAR>ContinuousConstSMul 𝕜 β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>c : 𝕜<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => c • f x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>𝕜 : Type u_5<VAR>TopologicalSpace 𝕜<VAR>VAdd 𝕜 β<VAR>ContinuousVAdd 𝕜 β<VAR>f : α → 𝕜<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>c : β<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => f x +ᵥ c) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>𝕜 : Type u_5<VAR>TopologicalSpace 𝕜<VAR>SMul 𝕜 β<VAR>ContinuousSMul 𝕜 β<VAR>f : α → 𝕜<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>c : β<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => f x • c) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>SemilatticeSup β<VAR>ContinuousSup β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEStronglyMeasurable (f ⊔ g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>SemilatticeInf β<VAR>ContinuousInf β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEStronglyMeasurable (f ⊓ g) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>M : Type u_5<VAR>AddMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable l.sum μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>M : Type u_5<VAR>Monoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable l.prod μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>M : Type u_5<VAR>AddMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => (List.map (fun f => f x) l).sum) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>M : Type u_5<VAR>Monoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => (List.map (fun f => f x) l).prod) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>M : Type u_5<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>l : Multiset (α → M)<VAR>hl : ∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable l.prod μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>l : Multiset (α → M)<VAR>hl : ∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable l.sum μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>M : Type u_5<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>s : Multiset (α → M)<VAR>hs : ∀ f ∈ s, MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => (Multiset.map (fun f => f x) s).prod) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>s : Multiset (α → M)<VAR>hs : ∀ f ∈ s, MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => (Multiset.map (fun f => f x) s).sum) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>ι : Type u_6<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ<GOAL>MeasureTheory.AEStronglyMeasurable (∑ i ∈ s, f i) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>M : Type u_5<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>ι : Type u_6<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ<GOAL>MeasureTheory.AEStronglyMeasurable (∏ i ∈ s, f i) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>M : Type u_5<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>ι : Type u_6<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun a => ∏ i ∈ s, f i a) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>ι : Type u_6<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun a => ∑ i ∈ s, f i a) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>MeasurableSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>OpensMeasurableSpace β<VAR>SecondCountableTopology β<VAR>hf : AEMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable f μ
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>TopologicalSpace.PseudoMetrizableSpace α<GOAL>∀ {x : MeasurableSpace α} [inst : OpensMeasurableSpace α] [inst : SecondCountableTopology α] {μ : MeasureTheory.Measure α}, MeasureTheory.AEStronglyMeasurable id μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>MeasurableSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>BorelSpace β<VAR>SecondCountableTopology β<GOAL>MeasureTheory.AEStronglyMeasurable f μ ↔ AEMeasurable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>PseudoMetricSpace β<VAR>f g : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => dist (f x) (g x)) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>SeminormedAddCommGroup β<VAR>f : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => ‖f x‖) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>SeminormedAddCommGroup β<VAR>f : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => ‖f x‖₊) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>SeminormedAddCommGroup β<VAR>f : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>AEMeasurable (fun a => ↑‖f a‖₊) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>SeminormedAddCommGroup β<VAR>f g : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>AEMeasurable (fun a => edist (f a) (g a)) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => (f x).toNNReal) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>Zero β<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.AEStronglyMeasurable (s.indicator f) μ ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>Zero β<VAR>hfm : MeasureTheory.AEStronglyMeasurable f μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.AEStronglyMeasurable (s.indicator f) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>TopologicalSpace E<VAR>TopologicalSpace.MetrizableSpace E<VAR>f g : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.NullMeasurableSet {x | f x = g x} μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>TopologicalSpace E<VAR>TopologicalSpace.MetrizableSpace E<VAR>Zero E<VAR>f : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.NullMeasurableSet (Function.support f) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>TopologicalSpace E<VAR>TopologicalSpace.MetrizableSpace E<VAR>One E<VAR>f : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.NullMeasurableSet (Function.mulSupport f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>LinearOrder β<VAR>OrderClosedTopology β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>f g : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.NullMeasurableSet {a | f a < g a} μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>OrderClosedTopology β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>f g : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.NullMeasurableSet {a | f a ≤ g a} μ
<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>α : Type u_5<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f (μ.trim hm)<GOAL>MeasureTheory.AEStronglyMeasurable f μ