ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>MeasurableSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>BorelSpace β<VAR>MeasurableSpace γ<VAR>TopologicalSpace.PseudoMetrizableSpace γ<VAR>BorelSpace γ<VAR>SecondCountableTopologyEither β γ<VAR>MeasurableSpace δ<VAR>TopologicalSpace.PseudoMetrizableSpace δ<VAR>OpensMeasurableSpace δ<VAR>SecondCountableTopology δ<VAR>g : β → γ → δ<VAR>hg : Measurable (Function.uncurry g)<VAR>f₁ : α → β<VAR>f₂ : α → γ<VAR>hf₁ : MeasureTheory.AEStronglyMeasurable f₁ μ<VAR>hf₂ : MeasureTheory.AEStronglyMeasurable f₂ μ<GOAL>MeasureTheory.AEEqFun.comp₂Measurable g hg (MeasureTheory.AEEqFun.mk f₁ hf₁) (MeasureTheory.AEEqFun.mk f₂ hf₂) = MeasureTheory.AEEqFun.mk (fun a => g (f₁ a) (f₂ a)) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>MeasurableSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>BorelSpace β<VAR>MeasurableSpace γ<VAR>TopologicalSpace.PseudoMetrizableSpace γ<VAR>BorelSpace γ<VAR>SecondCountableTopologyEither β γ<VAR>MeasurableSpace δ<VAR>TopologicalSpace.PseudoMetrizableSpace δ<VAR>OpensMeasurableSpace δ<VAR>SecondCountableTopology δ<VAR>g : β → γ → δ<VAR>hg : Measurable (Function.uncurry g)<VAR>f₁ : α →ₘ[μ] β<VAR>f₂ : α →ₘ[μ] γ<GOAL>MeasureTheory.AEEqFun.comp₂Measurable g hg f₁ f₂ = MeasureTheory.AEEqFun.compMeasurable (Function.uncurry g) hg (f₁.pair f₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>MeasurableSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>BorelSpace β<VAR>MeasurableSpace γ<VAR>TopologicalSpace.PseudoMetrizableSpace γ<VAR>BorelSpace γ<VAR>SecondCountableTopologyEither β γ<VAR>MeasurableSpace δ<VAR>TopologicalSpace.PseudoMetrizableSpace δ<VAR>OpensMeasurableSpace δ<VAR>SecondCountableTopology δ<VAR>g : β → γ → δ<VAR>hg : Measurable (Function.uncurry g)<VAR>f₁ : α →ₘ[μ] β<VAR>f₂ : α →ₘ[μ] γ<GOAL>MeasureTheory.AEEqFun.comp₂Measurable g hg f₁ f₂ = MeasureTheory.AEEqFun.mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>MeasurableSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>BorelSpace β<VAR>MeasurableSpace γ<VAR>TopologicalSpace.PseudoMetrizableSpace γ<VAR>BorelSpace γ<VAR>SecondCountableTopologyEither β γ<VAR>MeasurableSpace δ<VAR>TopologicalSpace.PseudoMetrizableSpace δ<VAR>OpensMeasurableSpace δ<VAR>SecondCountableTopology δ<VAR>g : β → γ → δ<VAR>hg : Measurable (Function.uncurry g)<VAR>f₁ : α →ₘ[μ] β<VAR>f₂ : α →ₘ[μ] γ<GOAL>↑(MeasureTheory.AEEqFun.comp₂Measurable g hg f₁ f₂) =ᵐ[μ] fun a => g (↑f₁ a) (↑f₂ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>(MeasureTheory.AEEqFun.mk f hf).toGerm = ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α →ₘ[μ] β<GOAL>f.toGerm = ↑↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<GOAL>Function.Injective MeasureTheory.AEEqFun.toGerm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>MeasurableSpace β<VAR>f : α → β<VAR>ν : MeasureTheory.Measure β<VAR>g : β →ₘ[ν] γ<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν<GOAL>(g.compQuasiMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>MeasurableSpace β<VAR>f : α → β<VAR>ν : MeasureTheory.Measure β<VAR>g : β →ₘ[ν] γ<VAR>hf : MeasureTheory.MeasurePreserving f μ ν<GOAL>(g.compMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>g : β → γ<VAR>hg : Continuous g<VAR>f : α →ₘ[μ] β<GOAL>(MeasureTheory.AEEqFun.comp g hg f).toGerm = Filter.Germ.map g f.toGerm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace γ<VAR>SecondCountableTopology γ<VAR>MeasurableSpace γ<VAR>OpensMeasurableSpace γ<VAR>g : β → γ<VAR>hg : Measurable g<VAR>f : α →ₘ[μ] β<GOAL>(MeasureTheory.AEEqFun.compMeasurable g hg f).toGerm = Filter.Germ.map g f.toGerm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>g : β → γ → δ<VAR>hg : Continuous (Function.uncurry g)<VAR>f₁ : α →ₘ[μ] β<VAR>f₂ : α →ₘ[μ] γ<GOAL>(MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂).toGerm = Filter.Germ.map₂ g f₁.toGerm f₂.toGerm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace γ<VAR>SecondCountableTopologyEither β γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>TopologicalSpace.PseudoMetrizableSpace δ<VAR>SecondCountableTopology δ<VAR>MeasurableSpace δ<VAR>OpensMeasurableSpace δ<VAR>g : β → γ → δ<VAR>hg : Measurable (Function.uncurry g)<VAR>f₁ : α →ₘ[μ] β<VAR>f₂ : α →ₘ[μ] γ<GOAL>(MeasureTheory.AEEqFun.comp₂Measurable g hg f₁ f₂).toGerm = Filter.Germ.map₂ g f₁.toGerm f₂.toGerm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>r : β → γ → Prop<VAR>f : α → β<VAR>g : α → γ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEEqFun.LiftRel r (MeasureTheory.AEEqFun.mk f hf) (MeasureTheory.AEEqFun.mk g hg) ↔ ∀ᵐ (a : α) ∂μ, r (f a) (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>r : β → γ → Prop<VAR>f : α →ₘ[μ] β<VAR>g : α →ₘ[μ] γ<GOAL>MeasureTheory.AEEqFun.LiftRel r f g ↔ ∀ᵐ (a : α) ∂μ, r (↑f a) (↑g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>f g : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEEqFun.mk f hf ≤ MeasureTheory.AEEqFun.mk g hg ↔ f ≤ᵐ[μ] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>f g : α →ₘ[μ] β<GOAL>↑f ≤ᵐ[μ] ↑g ↔ f ≤ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>SemilatticeSup β<VAR>ContinuousSup β<VAR>f g : α →ₘ[μ] β<GOAL>↑(f ⊔ g) =ᵐ[μ] fun x => ↑f x ⊔ ↑g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>SemilatticeSup β<VAR>ContinuousSup β<VAR>f g : α →ₘ[μ] β<GOAL>f ≤ f ⊔ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>SemilatticeSup β<VAR>ContinuousSup β<VAR>f g : α →ₘ[μ] β<GOAL>g ≤ f ⊔ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>SemilatticeSup β<VAR>ContinuousSup β<VAR>f g f' : α →ₘ[μ] β<VAR>hf : f ≤ f'<VAR>hg : g ≤ f'<GOAL>f ⊔ g ≤ f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>SemilatticeInf β<VAR>ContinuousInf β<VAR>f g : α →ₘ[μ] β<GOAL>↑(f ⊓ g) =ᵐ[μ] fun x => ↑f x ⊓ ↑g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>SemilatticeInf β<VAR>ContinuousInf β<VAR>f g : α →ₘ[μ] β<GOAL>f ⊓ g ≤ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>SemilatticeInf β<VAR>ContinuousInf β<VAR>f g : α →ₘ[μ] β<GOAL>f ⊓ g ≤ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>SemilatticeInf β<VAR>ContinuousInf β<VAR>f' f g : α →ₘ[μ] β<VAR>hf : f' ≤ f<VAR>hg : f' ≤ g<GOAL>f' ≤ f ⊓ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>b : β<GOAL>↑(MeasureTheory.AEEqFun.const α b) =ᵐ[μ] Function.const α b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>Zero β<GOAL>0 = MeasureTheory.AEEqFun.mk (fun x => 0) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>One β<GOAL>1 = MeasureTheory.AEEqFun.mk (fun x => 1) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>Zero β<GOAL>↑0 =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>One β<GOAL>↑1 =ᵐ[μ] 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>One β<GOAL>MeasureTheory.AEEqFun.toGerm 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>Zero β<GOAL>MeasureTheory.AEEqFun.toGerm 0 = 0
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>𝕜 : Type u_5<VAR>SMul 𝕜 γ<VAR>ContinuousConstSMul 𝕜 γ<VAR>c : 𝕜<VAR>f : α → γ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>c • MeasureTheory.AEEqFun.mk f hf = MeasureTheory.AEEqFun.mk (c • f) ⋯
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>𝕜 : Type u_5<VAR>SMul 𝕜 γ<VAR>ContinuousConstSMul 𝕜 γ<VAR>c : 𝕜<VAR>f : α →ₘ[μ] γ<GOAL>↑(c • f) =ᵐ[μ] c • ↑f
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>𝕜 : Type u_5<VAR>SMul 𝕜 γ<VAR>ContinuousConstSMul 𝕜 γ<VAR>c : 𝕜<VAR>f : α →ₘ[μ] γ<GOAL>(c • f).toGerm = c • f.toGerm
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Mul γ<VAR>ContinuousMul γ<VAR>f g : α → γ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEEqFun.mk f hf * MeasureTheory.AEEqFun.mk g hg = MeasureTheory.AEEqFun.mk (f * g) ⋯
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Add γ<VAR>ContinuousAdd γ<VAR>f g : α → γ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEEqFun.mk f hf + MeasureTheory.AEEqFun.mk g hg = MeasureTheory.AEEqFun.mk (f + g) ⋯
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Add γ<VAR>ContinuousAdd γ<VAR>f g : α →ₘ[μ] γ<GOAL>↑(f + g) =ᵐ[μ] ↑f + ↑g
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Mul γ<VAR>ContinuousMul γ<VAR>f g : α →ₘ[μ] γ<GOAL>↑(f * g) =ᵐ[μ] ↑f * ↑g
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Add γ<VAR>ContinuousAdd γ<VAR>f g : α →ₘ[μ] γ<GOAL>(f + g).toGerm = f.toGerm + g.toGerm
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Mul γ<VAR>ContinuousMul γ<VAR>f g : α →ₘ[μ] γ<GOAL>(f * g).toGerm = f.toGerm * g.toGerm
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Monoid γ<VAR>ContinuousMul γ<VAR>f : α → γ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>n : ℕ<GOAL>MeasureTheory.AEEqFun.mk f hf ^ n = MeasureTheory.AEEqFun.mk (f ^ n) ⋯
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Monoid γ<VAR>ContinuousMul γ<VAR>f : α →ₘ[μ] γ<VAR>n : ℕ<GOAL>↑(f ^ n) =ᵐ[μ] ↑f ^ n
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Monoid γ<VAR>ContinuousMul γ<VAR>f : α →ₘ[μ] γ<VAR>n : ℕ<GOAL>(f ^ n).toGerm = f.toGerm ^ n
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Monoid γ<VAR>ContinuousMul γ<VAR>f : α →ₘ[μ] γ<GOAL>MeasureTheory.AEEqFun.toGermMonoidHom f = f.toGerm
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>AddMonoid γ<VAR>ContinuousAdd γ<VAR>f : α →ₘ[μ] γ<GOAL>MeasureTheory.AEEqFun.toGermAddMonoidHom f = f.toGerm
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Group γ<VAR>TopologicalGroup γ<VAR>f : α → γ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>(MeasureTheory.AEEqFun.mk f hf)⁻¹ = MeasureTheory.AEEqFun.mk f⁻¹ ⋯
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>AddGroup γ<VAR>TopologicalAddGroup γ<VAR>f : α → γ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>-MeasureTheory.AEEqFun.mk f hf = MeasureTheory.AEEqFun.mk (-f) ⋯
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>AddGroup γ<VAR>TopologicalAddGroup γ<VAR>f : α →ₘ[μ] γ<GOAL>↑(-f) =ᵐ[μ] -↑f
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Group γ<VAR>TopologicalGroup γ<VAR>f : α →ₘ[μ] γ<GOAL>↑f⁻¹ =ᵐ[μ] (↑f)⁻¹
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Group γ<VAR>TopologicalGroup γ<VAR>f : α →ₘ[μ] γ<GOAL>f⁻¹.toGerm = f.toGerm⁻¹
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>AddGroup γ<VAR>TopologicalAddGroup γ<VAR>f : α →ₘ[μ] γ<GOAL>(-f).toGerm = -f.toGerm
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Group γ<VAR>TopologicalGroup γ<VAR>f g : α → γ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEEqFun.mk (f / g) ⋯ = MeasureTheory.AEEqFun.mk f hf / MeasureTheory.AEEqFun.mk g hg
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>AddGroup γ<VAR>TopologicalAddGroup γ<VAR>f g : α → γ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEEqFun.mk (f - g) ⋯ = MeasureTheory.AEEqFun.mk f hf - MeasureTheory.AEEqFun.mk g hg
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Group γ<VAR>TopologicalGroup γ<VAR>f g : α →ₘ[μ] γ<GOAL>↑(f / g) =ᵐ[μ] ↑f / ↑g
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>AddGroup γ<VAR>TopologicalAddGroup γ<VAR>f g : α →ₘ[μ] γ<GOAL>↑(f - g) =ᵐ[μ] ↑f - ↑g
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Group γ<VAR>TopologicalGroup γ<VAR>f g : α →ₘ[μ] γ<GOAL>(f / g).toGerm = f.toGerm / g.toGerm
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>AddGroup γ<VAR>TopologicalAddGroup γ<VAR>f g : α →ₘ[μ] γ<GOAL>(f - g).toGerm = f.toGerm - g.toGerm
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Group γ<VAR>TopologicalGroup γ<VAR>f : α → γ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>n : ℤ<GOAL>MeasureTheory.AEEqFun.mk f hf ^ n = MeasureTheory.AEEqFun.mk (f ^ n) ⋯
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Group γ<VAR>TopologicalGroup γ<VAR>f : α →ₘ[μ] γ<VAR>n : ℤ<GOAL>↑(f ^ n) =ᵐ[μ] ↑f ^ n
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>Group γ<VAR>TopologicalGroup γ<VAR>f : α →ₘ[μ] γ<VAR>n : ℤ<GOAL>(f ^ n).toGerm = f.toGerm ^ n
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>(MeasureTheory.AEEqFun.mk f hf).lintegral = ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α →ₘ[μ] ℝ≥0∞<GOAL>∫⁻ (a : α), ↑f a ∂μ = f.lintegral
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.AEEqFun.lintegral 0 = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α →ₘ[μ] ℝ≥0∞<GOAL>f.lintegral = 0 ↔ f = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α →ₘ[μ] ℝ≥0∞<GOAL>(f + g).lintegral = f.lintegral + g.lintegral
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α →ₘ[μ] ℝ≥0∞<GOAL>f ≤ g → f.lintegral ≤ g.lintegral
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>TopologicalSpace β<VAR>Lattice β<VAR>TopologicalLattice β<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>f : α →ₘ[μ] β<GOAL>↑|f| =ᵐ[μ] fun x => |↑f x|
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>LinearOrder γ<VAR>OrderClosedTopology γ<VAR>Zero γ<VAR>f : α → γ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>(MeasureTheory.AEEqFun.mk f hf).posPart = MeasureTheory.AEEqFun.mk (fun x => max (f x) 0) ⋯
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>LinearOrder γ<VAR>OrderClosedTopology γ<VAR>Zero γ<VAR>f : α →ₘ[μ] γ<GOAL>↑f.posPart =ᵐ[μ] fun a => max (↑f a) 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>TopologicalSpace β<VAR>SecondCountableTopologyEither α β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>f : C(α, β)<GOAL>↑(ContinuousMap.toAEEqFun μ f) =ᵐ[μ] ⇑f
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : MeasureTheory.Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>x : α<VAR>hx : x ∈ aeSeqSet hf p<VAR>i : ι<GOAL>AEMeasurable.mk (f i) ⋯ x = f i x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : MeasureTheory.Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>x : α<VAR>hx : x ∈ aeSeqSet hf p<VAR>i : ι<GOAL>aeSeq hf p i x = AEMeasurable.mk (f i) ⋯ x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : MeasureTheory.Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>x : α<VAR>hx : x ∈ aeSeqSet hf p<VAR>i : ι<GOAL>aeSeq hf p i x = f i x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : MeasureTheory.Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>x : α<VAR>hx : x ∈ aeSeqSet hf p<GOAL>p x fun n => aeSeq hf p n x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : MeasureTheory.Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>x : α<VAR>hx : x ∈ aeSeqSet hf p<GOAL>p x fun n => f n x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : MeasureTheory.Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<GOAL>MeasurableSet (aeSeqSet hf p)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : MeasureTheory.Measure α<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>p : α → (ι → β) → Prop<VAR>i : ι<GOAL>Measurable (aeSeq hf p i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : MeasureTheory.Measure α<VAR>p : α → (ι → β) → Prop<VAR>Countable ι<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x<GOAL>μ (aeSeqSet hf p)ᶜ = 0
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : MeasureTheory.Measure α<VAR>p : α → (ι → β) → Prop<VAR>Countable ι<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x<GOAL>∀ᵐ (a : α) ∂μ, ∀ (i : ι), aeSeq hf p i a = AEMeasurable.mk (f i) ⋯ a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : MeasureTheory.Measure α<VAR>p : α → (ι → β) → Prop<VAR>Countable ι<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x<GOAL>∀ᵐ (a : α) ∂μ, ∀ (i : ι), aeSeq hf p i a = f i a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : MeasureTheory.Measure α<VAR>p : α → (ι → β) → Prop<VAR>Countable ι<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x<VAR>n : ι<GOAL>aeSeq hf p n =ᵐ[μ] f n
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : MeasureTheory.Measure α<VAR>p : α → (ι → β) → Prop<VAR>CompleteLattice β<VAR>Countable ι<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x<GOAL>⨆ n, aeSeq hf p n =ᵐ[μ] ⨆ n, f n
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : MeasureTheory.Measure α<VAR>p : α → (ι → β) → Prop<VAR>CompleteLattice β<VAR>Countable ι<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x<GOAL>⨅ n, aeSeq hf p n =ᵐ[μ] ⨅ n, f n
<VAR>α : Type u_1<VAR>G : Type u_3<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>F : ℕ → α → G<VAR>f : α → G<VAR>bound : α → ℝ<VAR>F_measurable : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) μ<VAR>bound_integrable : MeasureTheory.Integrable bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))<GOAL>Filter.Tendsto (fun n => ∫ (a : α), F n a ∂μ) Filter.atTop (nhds (∫ (a : α), f a ∂μ))
<VAR>α : Type u_1<VAR>G : Type u_3<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_4<VAR>l : Filter ι<VAR>l.IsCountablyGenerated<VAR>F : ι → α → G<VAR>f : α → G<VAR>bound : α → ℝ<VAR>hF_meas : ∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (F n) μ<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>bound_integrable : MeasureTheory.Integrable bound μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) l (nhds (f a))<GOAL>Filter.Tendsto (fun n => ∫ (a : α), F n a ∂μ) l (nhds (∫ (a : α), f a ∂μ))