ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>y : β<GOAL>μ.prod (MeasureTheory.Measure.dirac y) = MeasureTheory.Measure.map (fun x => (x, y)) μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>x : α<GOAL>(MeasureTheory.Measure.dirac x).prod ν = MeasureTheory.Measure.map (Prod.mk x) ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>x : α<VAR>y : β<GOAL>(MeasureTheory.Measure.dirac x).prod (MeasureTheory.Measure.dirac y) = MeasureTheory.Measure.dirac (x, y)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>ν' : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν'<GOAL>μ.prod (ν + ν') = μ.prod ν + μ.prod ν'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>μ' : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ'<GOAL>(μ + μ').prod ν = μ.prod ν + μ'.prod ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<GOAL>MeasureTheory.Measure.prod 0 ν = 0
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<GOAL>μ.prod 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>δ : Type u_7<VAR>MeasurableSpace δ<VAR>f : α → β<VAR>g : γ → δ<VAR>μa : MeasureTheory.Measure α<VAR>μc : MeasureTheory.Measure γ<VAR>MeasureTheory.SFinite μa<VAR>MeasureTheory.SFinite μc<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>(MeasureTheory.Measure.map f μa).prod (MeasureTheory.Measure.map g μc) = MeasureTheory.Measure.map (Prod.map f g) (μa.prod μc)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>δ : Type u_7<VAR>MeasurableSpace δ<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>μc : MeasureTheory.Measure γ<VAR>μd : MeasureTheory.Measure δ<VAR>MeasureTheory.SFinite μa<VAR>MeasureTheory.SFinite μc<VAR>f : α → β<VAR>hf : MeasureTheory.MeasurePreserving f μa μb<VAR>g : α → γ → δ<VAR>hgm : Measurable (Function.uncurry g)<VAR>hg : ∀ᵐ (x : α) ∂μa, MeasureTheory.Measure.map (g x) μc = μd<GOAL>MeasureTheory.MeasurePreserving (fun p => (f p.1, g p.1 p.2)) (μa.prod μc) (μb.prod μd)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>δ : Type u_7<VAR>MeasurableSpace δ<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>μc : MeasureTheory.Measure γ<VAR>μd : MeasureTheory.Measure δ<VAR>MeasureTheory.SFinite μa<VAR>MeasureTheory.SFinite μc<VAR>f : α → β<VAR>g : γ → δ<VAR>hf : MeasureTheory.MeasurePreserving f μa μb<VAR>hg : MeasureTheory.MeasurePreserving g μc μd<GOAL>MeasureTheory.MeasurePreserving (Prod.map f g) (μa.prod μc) (μb.prod μd)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>f : α × β → γ<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>τ : MeasureTheory.Measure γ<VAR>hf : Measurable f<VAR>MeasureTheory.SFinite ν<VAR>h2f : ∀ᵐ (x : α) ∂μ, MeasureTheory.Measure.QuasiMeasurePreserving (fun y => f (x, y)) ν τ<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving f (μ.prod ν) τ
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>f : α × β → γ<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>τ : MeasureTheory.Measure γ<VAR>hf : Measurable f<VAR>MeasureTheory.SFinite μ<VAR>MeasureTheory.SFinite ν<VAR>h2f : ∀ᵐ (y : β) ∂ν, MeasureTheory.Measure.QuasiMeasurePreserving (fun x => f (x, y)) μ τ<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving f (μ.prod ν) τ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite μ<VAR>MeasureTheory.SFinite ν<VAR>f : β × α → γ<VAR>hf : AEMeasurable f (ν.prod μ)<GOAL>AEMeasurable (fun z => f z.swap) (μ.prod ν)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>f : α → γ<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun z => f z.1) (μ.prod ν)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>f : β → γ<VAR>hf : AEMeasurable f ν<GOAL>AEMeasurable (fun z => f z.2) (μ.prod ν)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>f : α × β → ℝ≥0∞<GOAL>∫⁻ (z : β × α), f z.swap ∂ν.prod μ = ∫⁻ (z : α × β), f z ∂μ.prod ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>f : α × β → ℝ≥0∞<GOAL>Measurable f → ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>f : α × β → ℝ≥0∞<VAR>hf : AEMeasurable f (μ.prod ν)<GOAL>∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>f : α × β → ℝ≥0∞<VAR>hf : AEMeasurable f (μ.prod ν)<GOAL>∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>f : α × β → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>f : α → β → ℝ≥0∞<VAR>hf : AEMeasurable (Function.uncurry f) (μ.prod ν)<GOAL>∫⁻ (x : α), ∫⁻ (y : β), f x y ∂ν ∂μ = ∫⁻ (z : α × β), f z.1 z.2 ∂μ.prod ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>f : α → β → ℝ≥0∞<VAR>hf : AEMeasurable (Function.uncurry f) (μ.prod ν)<GOAL>∫⁻ (x : α), ∫⁻ (y : β), f x y ∂ν ∂μ = ∫⁻ (z : β × α), f z.2 z.1 ∂ν.prod μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>f : α → β → ℝ≥0∞<VAR>hf : AEMeasurable (Function.uncurry f) (μ.prod ν)<GOAL>∫⁻ (x : α), ∫⁻ (y : β), f x y ∂ν ∂μ = ∫⁻ (y : β), ∫⁻ (x : α), f x y ∂μ ∂ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>f : α → ℝ≥0∞<VAR>g : β → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g ν<GOAL>∫⁻ (z : α × β), f z.1 * g z.2 ∂μ.prod ν = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ρ : MeasureTheory.Measure (α × β)<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>ρ.fst s = ρ (Prod.fst ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ρ : MeasureTheory.Measure (α × β)<GOAL>ρ.fst Set.univ = ρ Set.univ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<GOAL>MeasureTheory.Measure.fst 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.IsProbabilityMeasure ν<GOAL>(μ.prod ν).fst = μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>X : α → β<VAR>Y : α → γ<VAR>μ : MeasureTheory.Measure α<VAR>hY : AEMeasurable Y μ<GOAL>(MeasureTheory.Measure.map (fun a => (X a, Y a)) μ).fst = MeasureTheory.Measure.map X μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>X : α → β<VAR>Y : α → γ<VAR>μ : MeasureTheory.Measure α<VAR>hY : Measurable Y<GOAL>(MeasureTheory.Measure.map (fun a => (X a, Y a)) μ).fst = MeasureTheory.Measure.map X μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ρ : MeasureTheory.Measure (α × β)<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>ρ.snd s = ρ (Prod.snd ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ρ : MeasureTheory.Measure (α × β)<GOAL>ρ.snd Set.univ = ρ Set.univ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<GOAL>MeasureTheory.Measure.snd 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>(μ.prod ν).snd = ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>X : α → β<VAR>Y : α → γ<VAR>μ : MeasureTheory.Measure α<VAR>hX : AEMeasurable X μ<GOAL>(MeasureTheory.Measure.map (fun a => (X a, Y a)) μ).snd = MeasureTheory.Measure.map Y μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>X : α → β<VAR>Y : α → γ<VAR>μ : MeasureTheory.Measure α<VAR>hX : Measurable X<GOAL>(MeasureTheory.Measure.map (fun a => (X a, Y a)) μ).snd = MeasureTheory.Measure.map Y μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ρ : MeasureTheory.Measure (α × β)<GOAL>(MeasureTheory.Measure.map Prod.swap ρ).fst = ρ.snd
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ρ : MeasureTheory.Measure (α × β)<GOAL>(MeasureTheory.Measure.map Prod.swap ρ).snd = ρ.fst
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<GOAL>Measurable ⇑RCLike.re
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<GOAL>Measurable ⇑RCLike.im
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>m : MeasurableSpace α<VAR>f : α → 𝕜<VAR>hf : Measurable f<GOAL>Measurable fun x => RCLike.re (f x)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>m : MeasurableSpace α<VAR>f : α → 𝕜<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun x => RCLike.re (f x)) μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>m : MeasurableSpace α<VAR>f : α → 𝕜<VAR>hf : Measurable f<GOAL>Measurable fun x => RCLike.im (f x)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>m : MeasurableSpace α<VAR>f : α → 𝕜<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun x => RCLike.im (f x)) μ
<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<GOAL>Measurable RCLike.ofReal
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>MeasurableSpace α<VAR>f : α → 𝕜<VAR>hre : Measurable fun x => RCLike.re (f x)<VAR>him : Measurable fun x => RCLike.im (f x)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>MeasurableSpace α<VAR>f : α → 𝕜<VAR>μ : MeasureTheory.Measure α<VAR>hre : AEMeasurable (fun x => RCLike.re (f x)) μ<VAR>him : AEMeasurable (fun x => RCLike.im (f x)) μ<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_2<VAR>CompleteLinearOrder β<VAR>DenselyOrdered β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>SecondCountableTopology β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>s : Set β<VAR>s_count : s.Countable<VAR>s_dense : Dense s<VAR>f : α → β<VAR>h : ∀ p ∈ s, ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ∀ (p q : ℝ≥0), p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ μ (u ∩ v) = 0<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α →ₘ[μ] β<GOAL>MeasureTheory.StronglyMeasurable ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α →ₘ[μ] β<GOAL>MeasureTheory.AEStronglyMeasurable (↑f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>f : α →ₘ[μ] β<GOAL>Measurable ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>f : α →ₘ[μ] β<GOAL>AEMeasurable (↑f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>Quot.mk Setoid.r ⟨f, hf⟩ = MeasureTheory.AEEqFun.mk f hf
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<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>f : α →ₘ[μ] β<GOAL>MeasureTheory.AEEqFun.mk ↑f ⋯ = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α →ₘ[μ] β<VAR>h : ↑f =ᵐ[μ] ↑g<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α →ₘ[μ] β<GOAL>f = g ↔ ↑f =ᵐ[μ] ↑g
<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) =ᵐ[μ] f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α →ₘ[μ] β<VAR>p : (α →ₘ[μ] β) → Prop<VAR>H : ∀ (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ), p (MeasureTheory.AEEqFun.mk f hf)<GOAL>p f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>α' : Type u_5<VAR>β' : Type u_6<VAR>MeasurableSpace α'<VAR>TopologicalSpace β'<VAR>μ' : MeasureTheory.Measure α'<VAR>f : α →ₘ[μ] β<VAR>f' : α' →ₘ[μ'] β'<VAR>p : (α →ₘ[μ] β) → (α' →ₘ[μ'] β') → Prop<VAR>H : ∀ (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ) (f' : α' → β') (hf' : MeasureTheory.AEStronglyMeasurable f' μ'), p (MeasureTheory.AEEqFun.mk f hf) (MeasureTheory.AEEqFun.mk f' hf')<GOAL>p f f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>α' : Type u_5<VAR>β' : Type u_6<VAR>MeasurableSpace α'<VAR>TopologicalSpace β'<VAR>μ' : MeasureTheory.Measure α'<VAR>α'' : Type u_7<VAR>β'' : Type u_8<VAR>MeasurableSpace α''<VAR>TopologicalSpace β''<VAR>μ'' : MeasureTheory.Measure α''<VAR>f : α →ₘ[μ] β<VAR>f' : α' →ₘ[μ'] β'<VAR>f'' : α'' →ₘ[μ''] β''<VAR>p : (α →ₘ[μ] β) → (α' →ₘ[μ'] β') → (α'' →ₘ[μ''] β'') → Prop<VAR>H : ∀ (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ) (f' : α' → β') (hf' : MeasureTheory.AEStronglyMeasurable f' μ') (f'' : α'' → β'') (hf'' : MeasureTheory.AEStronglyMeasurable f'' μ''), p (MeasureTheory.AEEqFun.mk f hf) (MeasureTheory.AEEqFun.mk f' hf') (MeasureTheory.AEEqFun.mk f'' hf'')<GOAL>p f f' f''
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>f : α → β<VAR>g : β → γ<VAR>hg : MeasureTheory.AEStronglyMeasurable g ν<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν<GOAL>(MeasureTheory.AEEqFun.mk g hg).compQuasiMeasurePreserving f hf = MeasureTheory.AEEqFun.mk (g ∘ f) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>f : α → β<VAR>g : β →ₘ[ν] γ<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν<GOAL>g.compQuasiMeasurePreserving f hf = MeasureTheory.AEEqFun.mk (↑g ∘ f) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>f : α → β<VAR>g : β →ₘ[ν] γ<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν<GOAL>↑(g.compQuasiMeasurePreserving f hf) =ᵐ[μ] ↑g ∘ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>f : α → β<VAR>g : β → γ<VAR>hg : MeasureTheory.AEStronglyMeasurable g ν<VAR>hf : MeasureTheory.MeasurePreserving f μ ν<GOAL>(MeasureTheory.AEEqFun.mk g hg).compMeasurePreserving f hf = MeasureTheory.AEEqFun.mk (g ∘ f) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>f : α → β<VAR>g : β →ₘ[ν] γ<VAR>hf : MeasureTheory.MeasurePreserving f μ ν<GOAL>g.compMeasurePreserving f hf = MeasureTheory.AEEqFun.mk (↑g ∘ f) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace γ<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>f : α → β<VAR>g : β →ₘ[ν] γ<VAR>hf : MeasureTheory.MeasurePreserving f μ ν<GOAL>↑(g.compMeasurePreserving f hf) =ᵐ[μ] ↑g ∘ 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 : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEEqFun.comp g hg (MeasureTheory.AEEqFun.mk f hf) = MeasureTheory.AEEqFun.mk (g ∘ 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 = MeasureTheory.AEEqFun.mk (g ∘ ↑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) =ᵐ[μ] g ∘ ↑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>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>g : γ → δ<VAR>hg : Continuous g<VAR>f : β →ₘ[ν] γ<VAR>φ : α → β<VAR>hφ : MeasureTheory.Measure.QuasiMeasurePreserving φ μ ν<GOAL>(MeasureTheory.AEEqFun.comp g hg f).compQuasiMeasurePreserving φ hφ = MeasureTheory.AEEqFun.comp g hg (f.compQuasiMeasurePreserving φ hφ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>MeasurableSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>BorelSpace β<VAR>MeasurableSpace γ<VAR>TopologicalSpace.PseudoMetrizableSpace γ<VAR>OpensMeasurableSpace γ<VAR>SecondCountableTopology γ<VAR>g : β → γ<VAR>hg : Measurable g<VAR>f : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEEqFun.compMeasurable g hg (MeasureTheory.AEEqFun.mk f hf) = MeasureTheory.AEEqFun.mk (g ∘ f) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>MeasurableSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>BorelSpace β<VAR>MeasurableSpace γ<VAR>TopologicalSpace.PseudoMetrizableSpace γ<VAR>OpensMeasurableSpace γ<VAR>SecondCountableTopology γ<VAR>g : β → γ<VAR>hg : Measurable g<VAR>f : α →ₘ[μ] β<GOAL>MeasureTheory.AEEqFun.compMeasurable g hg f = MeasureTheory.AEEqFun.mk (g ∘ ↑f) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>MeasurableSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>BorelSpace β<VAR>MeasurableSpace γ<VAR>TopologicalSpace.PseudoMetrizableSpace γ<VAR>OpensMeasurableSpace γ<VAR>SecondCountableTopology γ<VAR>g : β → γ<VAR>hg : Measurable g<VAR>f : α →ₘ[μ] β<GOAL>↑(MeasureTheory.AEEqFun.compMeasurable g hg f) =ᵐ[μ] g ∘ ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>g : α → γ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>(MeasureTheory.AEEqFun.mk f hf).pair (MeasureTheory.AEEqFun.mk g hg) = MeasureTheory.AEEqFun.mk (fun x => (f x, g x)) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α →ₘ[μ] β<VAR>g : α →ₘ[μ] γ<GOAL>f.pair g = MeasureTheory.AEEqFun.mk (fun x => (↑f x, ↑g x)) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α →ₘ[μ] β<VAR>g : α →ₘ[μ] γ<GOAL>↑(f.pair g) =ᵐ[μ] fun x => (↑f x, ↑g x)
<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₂ : α → γ<VAR>hf₁ : MeasureTheory.AEStronglyMeasurable f₁ μ<VAR>hf₂ : MeasureTheory.AEStronglyMeasurable f₂ μ<GOAL>MeasureTheory.AEEqFun.comp₂ 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>g : β → γ → δ<VAR>hg : Continuous (Function.uncurry g)<VAR>f₁ : α →ₘ[μ] β<VAR>f₂ : α →ₘ[μ] γ<GOAL>MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂ = MeasureTheory.AEEqFun.comp (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>g : β → γ → δ<VAR>hg : Continuous (Function.uncurry g)<VAR>f₁ : α →ₘ[μ] β<VAR>f₂ : α →ₘ[μ] γ<GOAL>MeasureTheory.AEEqFun.comp₂ 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>g : β → γ → δ<VAR>hg : Continuous (Function.uncurry g)<VAR>f₁ : α →ₘ[μ] β<VAR>f₂ : α →ₘ[μ] γ<GOAL>↑(MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂) =ᵐ[μ] fun a => g (↑f₁ a) (↑f₂ a)