ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace β<GOAL>∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace γ} {f : α → γ → β}, MeasureTheory.StronglyMeasurable (Function.uncurry f) → ∀ {x : α}, MeasureTheory.StronglyMeasurable (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace β<GOAL>∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace γ} {f : α → γ → β}, MeasureTheory.StronglyMeasurable (Function.uncurry f) → ∀ {y : γ}, MeasureTheory.StronglyMeasurable fun x => f x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>Add β<VAR>ContinuousAdd β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<GOAL>MeasureTheory.StronglyMeasurable (f + g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>Mul β<VAR>ContinuousMul β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<GOAL>MeasureTheory.StronglyMeasurable (f * g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>Add β<VAR>ContinuousAdd β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>c : β<GOAL>MeasureTheory.StronglyMeasurable fun x => f x + c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>Mul β<VAR>ContinuousMul β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>c : β<GOAL>MeasureTheory.StronglyMeasurable fun x => f x * c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>Mul β<VAR>ContinuousMul β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>c : β<GOAL>MeasureTheory.StronglyMeasurable fun x => c * f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>Add β<VAR>ContinuousAdd β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>c : β<GOAL>MeasureTheory.StronglyMeasurable fun x => c + f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>Monoid β<VAR>ContinuousMul β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>n : ℕ<GOAL>MeasureTheory.StronglyMeasurable (f ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>AddMonoid β<VAR>ContinuousAdd β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>n : ℕ<GOAL>MeasureTheory.StronglyMeasurable (n • f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>Inv β<VAR>ContinuousInv β<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable f⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>Neg β<VAR>ContinuousNeg β<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable (-f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>Div β<VAR>ContinuousDiv β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<GOAL>MeasureTheory.StronglyMeasurable (f / g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>Sub β<VAR>ContinuousSub β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<GOAL>MeasureTheory.StronglyMeasurable (f - g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>CommGroup β<VAR>TopologicalGroup β<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable (f * g) ↔ MeasureTheory.StronglyMeasurable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>AddCommGroup β<VAR>TopologicalAddGroup β<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable (f + g) ↔ MeasureTheory.StronglyMeasurable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>CommGroup β<VAR>TopologicalGroup β<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable (g * f) ↔ MeasureTheory.StronglyMeasurable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>AddCommGroup β<VAR>TopologicalAddGroup β<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable (g + f) ↔ MeasureTheory.StronglyMeasurable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>𝕜 : Type u_5<VAR>TopologicalSpace 𝕜<VAR>VAdd 𝕜 β<VAR>ContinuousVAdd 𝕜 β<VAR>f : α → 𝕜<VAR>g : α → β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<GOAL>MeasureTheory.StronglyMeasurable fun x => f x +ᵥ g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>𝕜 : Type u_5<VAR>TopologicalSpace 𝕜<VAR>SMul 𝕜 β<VAR>ContinuousSMul 𝕜 β<VAR>f : α → 𝕜<VAR>g : α → β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<GOAL>MeasureTheory.StronglyMeasurable fun x => f x • g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>𝕜 : Type u_5<VAR>SMul 𝕜 β<VAR>ContinuousConstSMul 𝕜 β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>c : 𝕜<GOAL>MeasureTheory.StronglyMeasurable (c • f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>𝕜 : Type u_5<VAR>VAdd 𝕜 β<VAR>ContinuousConstVAdd 𝕜 β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>c : 𝕜<GOAL>MeasureTheory.StronglyMeasurable (c +ᵥ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>𝕜 : Type u_5<VAR>SMul 𝕜 β<VAR>ContinuousConstSMul 𝕜 β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>c : 𝕜<GOAL>MeasureTheory.StronglyMeasurable fun x => c • f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>𝕜 : Type u_5<VAR>VAdd 𝕜 β<VAR>ContinuousConstVAdd 𝕜 β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>c : 𝕜<GOAL>MeasureTheory.StronglyMeasurable fun x => c +ᵥ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>𝕜 : Type u_5<VAR>TopologicalSpace 𝕜<VAR>VAdd 𝕜 β<VAR>ContinuousVAdd 𝕜 β<VAR>f : α → 𝕜<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>c : β<GOAL>MeasureTheory.StronglyMeasurable fun x => f x +ᵥ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace β<VAR>𝕜 : Type u_5<VAR>TopologicalSpace 𝕜<VAR>SMul 𝕜 β<VAR>ContinuousSMul 𝕜 β<VAR>f : α → 𝕜<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>c : β<GOAL>MeasureTheory.StronglyMeasurable fun x => f x • c
<VAR>α : Type u_5<VAR>E : Type u_6<GOAL>∀ {x : MeasurableSpace α} [inst : AddGroup E] [inst_1 : TopologicalSpace E] [inst_2 : MeasurableSpace E] [inst_3 : BorelSpace E] [inst_4 : ContinuousAdd E] [inst_5 : TopologicalSpace.PseudoMetrizableSpace E] {g f : α → E}, Measurable g → MeasureTheory.StronglyMeasurable f → Measurable (g + f)
<VAR>α : Type u_5<VAR>E : Type u_6<GOAL>∀ {x : MeasurableSpace α} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : MeasurableSpace E] [inst_3 : BorelSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousNeg E] [inst_6 : TopologicalSpace.PseudoMetrizableSpace E] {g f : α → E}, Measurable g → MeasureTheory.StronglyMeasurable f → Measurable (g - f)
<VAR>α : Type u_5<VAR>E : Type u_6<GOAL>∀ {x : MeasurableSpace α} [inst : AddGroup E] [inst_1 : TopologicalSpace E] [inst_2 : MeasurableSpace E] [inst_3 : BorelSpace E] [inst_4 : ContinuousAdd E] [inst_5 : TopologicalSpace.PseudoMetrizableSpace E] {g f : α → E}, Measurable g → MeasureTheory.StronglyMeasurable f → Measurable (f + g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>G : Type u_6<VAR>TopologicalSpace β<VAR>Group G<VAR>MulAction G β<VAR>ContinuousConstSMul G β<VAR>m : MeasurableSpace α<VAR>c : G<GOAL>(MeasureTheory.StronglyMeasurable fun x => c • f x) ↔ MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>M : Type u_5<VAR>TopologicalSpace β<VAR>Monoid M<VAR>MulAction M β<VAR>ContinuousConstSMul M β<GOAL>∀ {x : MeasurableSpace α} {c : M}, IsUnit c → ((MeasureTheory.StronglyMeasurable fun x => c • f x) ↔ MeasureTheory.StronglyMeasurable f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>G₀ : Type u_7<VAR>TopologicalSpace β<VAR>GroupWithZero G₀<VAR>MulAction G₀ β<VAR>ContinuousConstSMul G₀ β<GOAL>∀ {x : MeasurableSpace α} {c : G₀}, c ≠ 0 → ((MeasureTheory.StronglyMeasurable fun x => c • f x) ↔ MeasureTheory.StronglyMeasurable f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>Sup β<VAR>ContinuousSup β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<GOAL>MeasureTheory.StronglyMeasurable (f ⊔ g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>Inf β<VAR>ContinuousInf β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<GOAL>MeasureTheory.StronglyMeasurable (f ⊓ g)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>m : MeasurableSpace α<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable l.sum
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Monoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>m : MeasurableSpace α<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable l.prod
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Monoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>m : MeasurableSpace α<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable fun x => (List.map (fun f => f x) l).prod
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>m : MeasurableSpace α<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable fun x => (List.map (fun f => f x) l).sum
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>m : MeasurableSpace α<VAR>l : Multiset (α → M)<VAR>hl : ∀ f ∈ l, MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable l.prod
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>m : MeasurableSpace α<VAR>l : Multiset (α → M)<VAR>hl : ∀ f ∈ l, MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable l.sum
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>m : MeasurableSpace α<VAR>s : Multiset (α → M)<VAR>hs : ∀ f ∈ s, MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable fun x => (Multiset.map (fun f => f x) s).sum
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>m : MeasurableSpace α<VAR>s : Multiset (α → M)<VAR>hs : ∀ f ∈ s, MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable fun x => (Multiset.map (fun f => f x) s).prod
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>m : MeasurableSpace α<VAR>ι : Type u_6<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, MeasureTheory.StronglyMeasurable (f i)<GOAL>MeasureTheory.StronglyMeasurable (∑ i ∈ s, f i)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>m : MeasurableSpace α<VAR>ι : Type u_6<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, MeasureTheory.StronglyMeasurable (f i)<GOAL>MeasureTheory.StronglyMeasurable (∏ i ∈ s, f i)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>m : MeasurableSpace α<VAR>ι : Type u_6<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, MeasureTheory.StronglyMeasurable (f i)<GOAL>MeasureTheory.StronglyMeasurable fun a => ∑ i ∈ s, f i a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>m : MeasurableSpace α<VAR>ι : Type u_6<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, MeasureTheory.StronglyMeasurable (f i)<GOAL>MeasureTheory.StronglyMeasurable fun a => ∏ i ∈ s, f i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>m : MeasurableSpace α<VAR>TopologicalSpace β<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>TopologicalSpace.IsSeparable (Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace.PseudoMetrizableSpace β], MeasureTheory.StronglyMeasurable f → ∀ {b : β}, TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {b})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>SecondCountableTopology β<VAR>OpensMeasurableSpace β<VAR>hf : Measurable f<GOAL>MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>TopologicalSpace.MetrizableSpace β<VAR>BorelSpace β<VAR>SecondCountableTopology β<GOAL>MeasureTheory.StronglyMeasurable f ↔ Measurable f
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>TopologicalSpace α<VAR>TopologicalSpace.PseudoMetrizableSpace α<VAR>OpensMeasurableSpace α<VAR>SecondCountableTopology α<GOAL>MeasureTheory.StronglyMeasurable id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>m : MeasurableSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<GOAL>MeasureTheory.StronglyMeasurable f ↔ Measurable f ∧ TopologicalSpace.IsSeparable (Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>h : SecondCountableTopologyEither α β<VAR>f : α → β<VAR>hf : Continuous f<GOAL>MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>BorelSpace β<VAR>Zero β<VAR>f : α → β<VAR>hf : Continuous f<VAR>k : Set α<VAR>hk : IsCompact k<VAR>h'f : Function.support f ⊆ k<GOAL>MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>BorelSpace β<VAR>One β<VAR>f : α → β<VAR>hf : Continuous f<VAR>k : Set α<VAR>hk : IsCompact k<VAR>h'f : Function.mulSupport f ⊆ k<GOAL>MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>BorelSpace β<VAR>One β<VAR>f : α → β<VAR>hf : Continuous f<VAR>h'f : HasCompactMulSupport f<GOAL>MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>BorelSpace β<VAR>Zero β<VAR>f : α → β<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<GOAL>MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_1<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>Zero α<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>MeasurableSpace X<VAR>MeasurableSpace Y<VAR>OpensMeasurableSpace X<VAR>OpensMeasurableSpace Y<VAR>TopologicalSpace α<VAR>TopologicalSpace.PseudoMetrizableSpace α<VAR>f : X × Y → α<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<GOAL>MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace.PseudoMetrizableSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : Embedding g<GOAL>(MeasureTheory.StronglyMeasurable fun x => g (f x)) ↔ MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>u : Filter ι<VAR>u.NeBot<VAR>u.IsCountablyGenerated<VAR>f : ι → α → β<VAR>g : α → β<VAR>hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)<VAR>lim : Filter.Tendsto f u (𝓝 g)<GOAL>MeasureTheory.StronglyMeasurable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>TopologicalSpace β<VAR>s : Set α<GOAL>∀ {x : DecidablePred fun x => x ∈ s}, MeasurableSet s → MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable (s.piecewise f g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<GOAL>∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] {p : α → Prop} {x_1 : DecidablePred p}, MeasurableSet {a | p a} → MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun x => if p x then f x else g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : α → γ<VAR>g' : γ → β<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>TopologicalSpace β<VAR>hg : MeasurableEmbedding g<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg' : MeasureTheory.StronglyMeasurable g'<GOAL>MeasureTheory.StronglyMeasurable (Function.extend g f g')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : α → γ<GOAL>∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace γ} [inst : TopologicalSpace β], MeasurableEmbedding g → MeasureTheory.StronglyMeasurable f → (γ → Nonempty β) → ∃ f', MeasureTheory.StronglyMeasurable f' ∧ f' ∘ g = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>h : Set.univ ⊆ s ∪ t<VAR>hc : MeasureTheory.StronglyMeasurable fun a => f ↑a<VAR>hd : MeasureTheory.StronglyMeasurable fun a => f ↑a<GOAL>MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] {f : α → β} {s : Set α}, MeasurableSet s → MeasureTheory.StronglyMeasurable (s.restrict f) → MeasureTheory.StronglyMeasurable (sᶜ.restrict f) → MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Zero β], MeasureTheory.StronglyMeasurable f → ∀ {s : Set α}, MeasurableSet s → MeasureTheory.StronglyMeasurable (s.indicator f)
<VAR>α : Type u_1<GOAL>∀ {x : MeasurableSpace α} {β : Type u_5} [inst : PseudoMetricSpace β] {f g : α → β}, MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun x => dist (f x) (g x)
<VAR>α : Type u_1<GOAL>∀ {x : MeasurableSpace α} {β : Type u_5} [inst : SeminormedAddCommGroup β] {f : α → β}, MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => ‖f x‖
<VAR>α : Type u_1<GOAL>∀ {x : MeasurableSpace α} {β : Type u_5} [inst : SeminormedAddCommGroup β] {f : α → β}, MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => ‖f x‖₊
<VAR>α : Type u_1<GOAL>∀ {x : MeasurableSpace α} {β : Type u_5} [inst : SeminormedAddCommGroup β] {f : α → β}, MeasureTheory.StronglyMeasurable f → Measurable fun a => ↑‖f a‖₊
<VAR>α : Type u_1<GOAL>∀ {x : MeasurableSpace α} {f : α → ℝ}, MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => (f x).toNNReal
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>E : Type u_5<VAR>TopologicalSpace E<VAR>TopologicalSpace.MetrizableSpace E<VAR>f g : α → E<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<GOAL>MeasurableSet {x | f x = g x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>TopologicalSpace β<VAR>LinearOrder β<VAR>OrderClosedTopology β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>f g : α → β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<GOAL>MeasurableSet {a | f a < g a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>OrderClosedTopology β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>f g : α → β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<GOAL>MeasurableSet {a | f a ≤ g a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>s : Set α<VAR>f : α → β<VAR>hs : MeasurableSet s<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hf_zero : ∀ x ∉ s, f x = 0<GOAL>∃ fs, (∀ (x : α), Filter.Tendsto (fun n => ↑(fs n) x) Filter.atTop (𝓝 (f x))) ∧ ∀ x ∉ s, ∀ (n : ℕ), ↑(fs n) x = 0
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>m m₂ : MeasurableSpace α<VAR>TopologicalSpace E<VAR>Zero E<VAR>s : Set α<VAR>f : α → E<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hf_zero : ∀ x ∉ s, f x = 0<GOAL>MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>SeminormedAddCommGroup β<VAR>m m0 : MeasurableSpace α<VAR>hm : m ≤ m0<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<GOAL>∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ μ (s n) < ⊤ ∧ ∀ x ∈ s n, ‖f x‖ ≤ ↑n) ∧ ⋃ i, s i = Set.univ
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Zero β<VAR>TopologicalSpace β<GOAL>MeasureTheory.FinStronglyMeasurable 0 μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>Zero β<VAR>TopologicalSpace β<VAR>hf : MeasureTheory.FinStronglyMeasurable f μ<GOAL>MeasureTheory.AEFinStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>Zero β<VAR>TopologicalSpace β<VAR>hf : MeasureTheory.FinStronglyMeasurable f μ<VAR>n : ℕ<GOAL>μ (Function.support ↑(hf.approx n)) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>Zero β<VAR>TopologicalSpace β<VAR>hf : MeasureTheory.FinStronglyMeasurable f μ<VAR>x : α<GOAL>Filter.Tendsto (fun n => ↑(hf.approx n) x) Filter.atTop (𝓝 (f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>Zero β<VAR>TopologicalSpace β<VAR>hf : MeasureTheory.FinStronglyMeasurable f μ<GOAL>MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>Zero β<VAR>TopologicalSpace β<VAR>T2Space β<VAR>hf : MeasureTheory.FinStronglyMeasurable f μ<GOAL>∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ MeasureTheory.SigmaFinite (μ.restrict t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>Zero β<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>hf : MeasureTheory.FinStronglyMeasurable f μ<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → β<VAR>TopologicalSpace β<VAR>MonoidWithZero β<VAR>ContinuousMul β<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>AddMonoid β<VAR>ContinuousAdd β<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>AddGroup β<VAR>TopologicalAddGroup β<VAR>hf : MeasureTheory.FinStronglyMeasurable f μ<GOAL>MeasureTheory.FinStronglyMeasurable (-f) μ