ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>ι : Sort u_4<VAR>f : α → β<VAR>m : ι → MeasureTheory.OuterMeasure α<GOAL>(MeasureTheory.OuterMeasure.map f) (⨆ i, m i) = ⨆ i, (MeasureTheory.OuterMeasure.map f) (m i)
<VAR>α : Type u_1<VAR>a : α<VAR>s : Set α<GOAL>(MeasureTheory.OuterMeasure.dirac a) s = s.indicator (fun x => 1) a
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>f : ι → MeasureTheory.OuterMeasure α<VAR>s : Set α<GOAL>(MeasureTheory.OuterMeasure.sum f) s = ∑' (i : ι), (f i) s
<VAR>α : Type u_1<VAR>a : ℝ≥0∞<VAR>b : α<VAR>s : Set α<GOAL>(a • MeasureTheory.OuterMeasure.dirac b) s = s.indicator (fun x => a) b
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : α → β<VAR>m : MeasureTheory.OuterMeasure β<VAR>s : Set α<GOAL>((MeasureTheory.OuterMeasure.comap f) m) s = m (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : α → β<GOAL>Monotone ⇑(MeasureTheory.OuterMeasure.comap f)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>ι : Sort u_4<VAR>f : α → β<VAR>m : ι → MeasureTheory.OuterMeasure β<GOAL>(MeasureTheory.OuterMeasure.comap f) (⨆ i, m i) = ⨆ i, (MeasureTheory.OuterMeasure.comap f) (m i)
<VAR>α : Type u_1<VAR>s t : Set α<VAR>m : MeasureTheory.OuterMeasure α<GOAL>((MeasureTheory.OuterMeasure.restrict s) m) t = m (t ∩ s)
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>m m' : MeasureTheory.OuterMeasure α<VAR>hm : m ≤ m'<GOAL>(MeasureTheory.OuterMeasure.restrict s) m ≤ (MeasureTheory.OuterMeasure.restrict t) m'
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<GOAL>(MeasureTheory.OuterMeasure.restrict Set.univ) m = m
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<GOAL>(MeasureTheory.OuterMeasure.restrict ∅) m = 0
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>s : Set α<VAR>m : ι → MeasureTheory.OuterMeasure α<GOAL>(MeasureTheory.OuterMeasure.restrict s) (⨆ i, m i) = ⨆ i, (MeasureTheory.OuterMeasure.restrict s) (m i)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : α → β<VAR>m : MeasureTheory.OuterMeasure β<GOAL>(MeasureTheory.OuterMeasure.map f) ((MeasureTheory.OuterMeasure.comap f) m) = (MeasureTheory.OuterMeasure.restrict (Set.range f)) m
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : α → β<VAR>m : MeasureTheory.OuterMeasure β<GOAL>(MeasureTheory.OuterMeasure.map f) ((MeasureTheory.OuterMeasure.comap f) m) ≤ m
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : Set α<GOAL>(MeasureTheory.OuterMeasure.restrict s) m ≤ m
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>ma : MeasureTheory.OuterMeasure α<VAR>mb : MeasureTheory.OuterMeasure β<VAR>f : α → β<GOAL>(MeasureTheory.OuterMeasure.map f) ma ≤ (MeasureTheory.OuterMeasure.restrict (Set.range f)) mb ↔ (MeasureTheory.OuterMeasure.map f) ma ≤ mb
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>m : MeasureTheory.OuterMeasure β<GOAL>(MeasureTheory.OuterMeasure.map f) ((MeasureTheory.OuterMeasure.comap f) m) = m
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : α → β<VAR>m : MeasureTheory.OuterMeasure α<GOAL>m ≤ (MeasureTheory.OuterMeasure.comap f) ((MeasureTheory.OuterMeasure.map f) m)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>m : MeasureTheory.OuterMeasure α<GOAL>(MeasureTheory.OuterMeasure.comap f) ((MeasureTheory.OuterMeasure.map f) m) = m
<VAR>α : Type u_1<VAR>s : Set α<VAR>h : s.Nonempty<GOAL>⊤ s = ⊤
<VAR>α : Type u_1<VAR>s : Set α<GOAL>⊤ s = ⨅ (_ : s = ∅), 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>(MeasureTheory.OuterMeasure.comap f) ⊤ = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>(MeasureTheory.OuterMeasure.map f) ⊤ = (MeasureTheory.OuterMeasure.restrict (Set.range f)) ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>(MeasureTheory.OuterMeasure.map f) ⊤ = ⊤
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>CompleteSpace E'<VAR>NormedSpace ℝ E'<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.lpMeas E' 𝕜 m p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑↑f) s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0<GOAL>↑↑↑f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>CompleteSpace E'<VAR>NormedSpace ℝ E'<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.Lp E' p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑f) s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0<VAR>hf_meas : MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ<GOAL>↑↑f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>CompleteSpace E'<VAR>NormedSpace ℝ E'<VAR>hm : m ≤ m0<VAR>f g : ↥(MeasureTheory.Lp E' p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑f) s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑g) s μ<VAR>hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ<VAR>hf_meas : MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ<VAR>hg_meas : MeasureTheory.AEStronglyMeasurable' m (↑↑g) μ<GOAL>↑↑f =ᵐ[μ] ↑↑g
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn g s μ<VAR>hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<VAR>hfm : MeasureTheory.AEStronglyMeasurable' m f μ<VAR>hgm : MeasureTheory.AEStronglyMeasurable' m g μ<GOAL>f =ᵐ[μ] g
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>f g : α → ℝ<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hfi : MeasureTheory.IntegrableOn f s μ<VAR>hg : MeasureTheory.StronglyMeasurable g<VAR>hgi : MeasureTheory.IntegrableOn g s μ<VAR>hgf : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>∫ (x : α) in s, ‖g x‖ ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ∂μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>f g : α → ℝ<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hfi : MeasureTheory.IntegrableOn f s μ<VAR>hg : MeasureTheory.StronglyMeasurable g<VAR>hgi : MeasureTheory.IntegrableOn g s μ<VAR>hgf : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>∫⁻ (x : α) in s, ↑‖g x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖f x‖₊ ∂μ
<VAR>α : Type u<VAR>MeasurableSpace α<VAR>β : Type v<VAR>self : MeasureTheory.SimpleFunc α β<GOAL>(Set.range ↑self).Finite
<VAR>α : Type u<VAR>MeasurableSpace α<VAR>β : Type v<VAR>self : MeasureTheory.SimpleFunc α β<VAR>x : β<GOAL>MeasurableSet (↑self ⁻¹' {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f g : MeasureTheory.SimpleFunc α β<VAR>H : ↑f = ↑g<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f g : MeasureTheory.SimpleFunc α β<VAR>H : ∀ (a : α), ↑f a = ↑g a<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>(Set.range ↑f).Finite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>x : β<GOAL>MeasurableSet (↑f ⁻¹' {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f : α → β<VAR>h : ∀ (x : β), MeasurableSet (f ⁻¹' {x})<VAR>h' : (Set.range f).Finite<VAR>x : α<GOAL>↑{ toFun := f, measurableSet_fiber' := h, finite_range' := h' } x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>b : β<GOAL>b ∈ f.range ↔ b ∈ Set.range ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>x : α<GOAL>↑f x ∈ f.range
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>↑f.range = Set.range ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>x : β<VAR>μ : MeasureTheory.Measure α<VAR>H : μ (↑f ⁻¹' {x}) ≠ 0<GOAL>x ∈ f.range
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>p : β → Prop<GOAL>(∀ y ∈ f.range, p y) ↔ ∀ (x : α), p (↑f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>p : β → Prop<GOAL>(∃ y ∈ f.range, p y) ↔ ∃ x, p (↑f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>b : β<GOAL>↑f ⁻¹' {b} = ∅ ↔ b ∉ f.range
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Nonempty β<VAR>Preorder β<VAR>IsDirected β fun x x_1 => x ≤ x_1<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>∃ C, ∀ (x : α), ↑f x ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>a : α<VAR>b : β<GOAL>↑(MeasureTheory.SimpleFunc.const α b) a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>b : β<GOAL>↑(MeasureTheory.SimpleFunc.const α b) = Function.const α b
<VAR>β : Type u_2<VAR>α : Type u_5<VAR>MeasurableSpace α<VAR>Nonempty α<VAR>b : β<GOAL>(MeasureTheory.SimpleFunc.const α b).range = {b}
<VAR>β : Type u_2<VAR>α : Type u_5<VAR>MeasurableSpace α<VAR>b : β<GOAL>(MeasureTheory.SimpleFunc.const α b).range ⊆ {b}
<VAR>β : Type u_2<VAR>α : Type u_5<VAR>f : MeasureTheory.SimpleFunc α β<VAR>Nonempty β<GOAL>∃ c, ∀ (x : α), ↑f x = c
<VAR>β : Type u_2<VAR>α : Type u_5<VAR>Nonempty β<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>∃ c, f = MeasureTheory.SimpleFunc.const α c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>r : α → β → Prop<VAR>f : MeasureTheory.SimpleFunc α β<VAR>h : ∀ (b : β), MeasurableSet {a | r a b}<GOAL>MeasurableSet {a | r a (↑f a)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>s : Set β<GOAL>MeasurableSet (↑f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>Measurable ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>AEMeasurable (↑f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>μ : MeasureTheory.Measure α<VAR>s : Finset β<GOAL>∑ y ∈ s, μ (↑f ⁻¹' {y}) = μ (↑f ⁻¹' ↑s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>μ : MeasureTheory.Measure α<GOAL>∑ y ∈ f.range, μ (↑f ⁻¹' {y}) = μ Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f g : MeasureTheory.SimpleFunc α β<GOAL>↑(MeasureTheory.SimpleFunc.piecewise s hs f g) = s.piecewise ↑f ↑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f g : MeasureTheory.SimpleFunc α β<VAR>a : α<GOAL>↑(MeasureTheory.SimpleFunc.piecewise s hs f g) a = if a ∈ s then ↑f a else ↑g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet sᶜ<VAR>f g : MeasureTheory.SimpleFunc α β<GOAL>MeasureTheory.SimpleFunc.piecewise sᶜ hs f g = MeasureTheory.SimpleFunc.piecewise s ⋯ g f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f g : MeasureTheory.SimpleFunc α β<GOAL>MeasureTheory.SimpleFunc.piecewise Set.univ ⋯ f g = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f g : MeasureTheory.SimpleFunc α β<GOAL>MeasureTheory.SimpleFunc.piecewise ∅ ⋯ f g = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.SimpleFunc.piecewise s hs f f = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Zero β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>Function.support ↑(MeasureTheory.SimpleFunc.piecewise s hs f (MeasureTheory.SimpleFunc.const α 0)) = s ∩ Function.support ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs_nonempty : s.Nonempty<VAR>hs_ne_univ : s ≠ Set.univ<VAR>x y : β<GOAL>(MeasureTheory.SimpleFunc.piecewise s hs (MeasureTheory.SimpleFunc.const α x) (MeasureTheory.SimpleFunc.const α y)).range = {x, y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace γ<VAR>f : MeasureTheory.SimpleFunc α β<VAR>g : β → α → γ<VAR>hg : ∀ (b : β), Measurable (g b)<GOAL>Measurable fun a => g (↑f a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>g : β → MeasureTheory.SimpleFunc α γ<VAR>a : α<GOAL>↑(f.bind g) a = ↑(g (↑f a)) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>g : β → γ<VAR>f : MeasureTheory.SimpleFunc α β<VAR>a : α<GOAL>↑(MeasureTheory.SimpleFunc.map g f) a = g (↑f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>MeasurableSpace α<VAR>g : β → γ<VAR>h : γ → δ<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>MeasureTheory.SimpleFunc.map h (MeasureTheory.SimpleFunc.map g f) = MeasureTheory.SimpleFunc.map (h ∘ g) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>g : β → γ<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>↑(MeasureTheory.SimpleFunc.map g f) = g ∘ ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>DecidableEq γ<VAR>g : β → γ<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>(MeasureTheory.SimpleFunc.map g f).range = Finset.image g f.range
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>g : β → γ<VAR>b : β<GOAL>MeasureTheory.SimpleFunc.map g (MeasureTheory.SimpleFunc.const α b) = MeasureTheory.SimpleFunc.const α (g b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>g : β → γ<VAR>s : Set γ<GOAL>↑(MeasureTheory.SimpleFunc.map g f) ⁻¹' s = ↑f ⁻¹' ↑(Finset.filter (fun b => g b ∈ s) f.range)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>g : β → γ<VAR>c : γ<GOAL>↑(MeasureTheory.SimpleFunc.map g f) ⁻¹' {c} = ↑f ⁻¹' ↑(Finset.filter (fun b => g b = c) f.range)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : MeasureTheory.SimpleFunc β γ<VAR>g : α → β<VAR>hgm : Measurable g<GOAL>↑(f.comp g hgm) = ↑f ∘ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : MeasureTheory.SimpleFunc β γ<VAR>g : α → β<VAR>hgm : Measurable g<GOAL>(f.comp g hgm).range ⊆ f.range
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f₁ : MeasureTheory.SimpleFunc α γ<VAR>g : α → β<VAR>hg : MeasurableEmbedding g<VAR>f₂ : MeasureTheory.SimpleFunc β γ<VAR>x : α<GOAL>↑(f₁.extend g hg f₂) (g x) = ↑f₁ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f₁ : MeasureTheory.SimpleFunc α γ<VAR>g : α → β<VAR>hg : MeasurableEmbedding g<VAR>f₂ : MeasureTheory.SimpleFunc β γ<VAR>y : β<VAR>h : ¬∃ x, g x = y<GOAL>↑(f₁.extend g hg f₂) y = ↑f₂ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f₁ : MeasureTheory.SimpleFunc α γ<VAR>g : α → β<VAR>hg : MeasurableEmbedding g<VAR>f₂ : MeasureTheory.SimpleFunc β γ<GOAL>↑(f₁.extend g hg f₂) ∘ g = ↑f₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f₁ : MeasureTheory.SimpleFunc α γ<VAR>g : α → β<VAR>hg : MeasurableEmbedding g<VAR>f₂ : MeasureTheory.SimpleFunc β γ<GOAL>(f₁.extend g hg f₂).comp g ⋯ = f₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α (β → γ)<VAR>g : MeasureTheory.SimpleFunc α β<VAR>a : α<GOAL>↑(f.seq g) a = ↑f a (↑g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>g : MeasureTheory.SimpleFunc α γ<VAR>a : α<GOAL>↑(f.pair g) a = (↑f a, ↑g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>g : MeasureTheory.SimpleFunc α γ<VAR>s : Set β<VAR>t : Set γ<GOAL>↑(f.pair g) ⁻¹' s ×ˢ t = ↑f ⁻¹' s ∩ ↑g ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>g : MeasureTheory.SimpleFunc α γ<VAR>b : β<VAR>c : γ<GOAL>↑(f.pair g) ⁻¹' {(b, c)} = ↑f ⁻¹' {b} ∩ ↑g ⁻¹' {c}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>f.bind (MeasureTheory.SimpleFunc.const α) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Zero β<GOAL>MeasureTheory.SimpleFunc.const α 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>One β<GOAL>MeasureTheory.SimpleFunc.const α 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>One β<GOAL>↑1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Zero β<GOAL>↑0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Mul β<VAR>f g : MeasureTheory.SimpleFunc α β<GOAL>↑(f * g) = ↑f * ↑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Add β<VAR>f g : MeasureTheory.SimpleFunc α β<GOAL>↑(f + g) = ↑f + ↑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Neg β<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>↑(-f) = -↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Inv β<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>↑f⁻¹ = (↑f)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Div β<VAR>f g : MeasureTheory.SimpleFunc α β<GOAL>↑(f / g) = ↑f / ↑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Sub β<VAR>f g : MeasureTheory.SimpleFunc α β<GOAL>↑(f - g) = ↑f - ↑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Preorder β<VAR>f g : MeasureTheory.SimpleFunc α β<GOAL>↑f ≤ ↑g ↔ f ≤ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Sup β<VAR>f g : MeasureTheory.SimpleFunc α β<GOAL>↑(f ⊔ g) = ↑f ⊔ ↑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Inf β<VAR>f g : MeasureTheory.SimpleFunc α β<GOAL>↑(f ⊓ g) = ↑f ⊓ ↑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Add β<VAR>f g : MeasureTheory.SimpleFunc α β<VAR>a : α<GOAL>↑(f + g) a = ↑f a + ↑g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Mul β<VAR>f g : MeasureTheory.SimpleFunc α β<VAR>a : α<GOAL>↑(f * g) a = ↑f a * ↑g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Sub β<VAR>f g : MeasureTheory.SimpleFunc α β<VAR>x : α<GOAL>↑(f - g) x = ↑f x - ↑g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Div β<VAR>f g : MeasureTheory.SimpleFunc α β<VAR>x : α<GOAL>↑(f / g) x = ↑f x / ↑g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Inv β<VAR>f : MeasureTheory.SimpleFunc α β<VAR>x : α<GOAL>↑f⁻¹ x = (↑f x)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Neg β<VAR>f : MeasureTheory.SimpleFunc α β<VAR>x : α<GOAL>↑(-f) x = -↑f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Sup β<VAR>f g : MeasureTheory.SimpleFunc α β<VAR>a : α<GOAL>↑(f ⊔ g) a = ↑f a ⊔ ↑g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Inf β<VAR>f g : MeasureTheory.SimpleFunc α β<VAR>a : α<GOAL>↑(f ⊓ g) a = ↑f a ⊓ ↑g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Nonempty α<VAR>Zero β<GOAL>MeasureTheory.SimpleFunc.range 0 = {0}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Nonempty α<VAR>One β<GOAL>MeasureTheory.SimpleFunc.range 1 = {1}
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_5<VAR>hα : IsEmpty α<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>f.range = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Zero β<VAR>y : β<GOAL>y ∈ MeasureTheory.SimpleFunc.range 0 → y = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Add β<VAR>f g : MeasureTheory.SimpleFunc α β<GOAL>f + g = MeasureTheory.SimpleFunc.map (fun p => p.1 + p.2) (f.pair g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Mul β<VAR>f g : MeasureTheory.SimpleFunc α β<GOAL>f * g = MeasureTheory.SimpleFunc.map (fun p => p.1 * p.2) (f.pair g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Sup β<VAR>f g : MeasureTheory.SimpleFunc α β<GOAL>f ⊔ g = MeasureTheory.SimpleFunc.map (fun p => p.1 ⊔ p.2) (f.pair g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Add β<VAR>f : MeasureTheory.SimpleFunc α β<VAR>b : β<GOAL>MeasureTheory.SimpleFunc.const α b + f = MeasureTheory.SimpleFunc.map (fun a => b + a) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Mul β<VAR>f : MeasureTheory.SimpleFunc α β<VAR>b : β<GOAL>MeasureTheory.SimpleFunc.const α b * f = MeasureTheory.SimpleFunc.map (fun a => b * a) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>Add β<VAR>Add γ<VAR>g : β → γ<VAR>hg : ∀ (x y : β), g (x + y) = g x + g y<VAR>f₁ f₂ : MeasureTheory.SimpleFunc α β<GOAL>MeasureTheory.SimpleFunc.map g (f₁ + f₂) = MeasureTheory.SimpleFunc.map g f₁ + MeasureTheory.SimpleFunc.map g f₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>Mul β<VAR>Mul γ<VAR>g : β → γ<VAR>hg : ∀ (x y : β), g (x * y) = g x * g y<VAR>f₁ f₂ : MeasureTheory.SimpleFunc α β<GOAL>MeasureTheory.SimpleFunc.map g (f₁ * f₂) = MeasureTheory.SimpleFunc.map g f₁ * MeasureTheory.SimpleFunc.map g f₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>K : Type u_5<VAR>SMul K β<VAR>c : K<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>↑(c • f) = c • ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>K : Type u_5<VAR>VAdd K β<VAR>c : K<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>↑(c +ᵥ f) = c +ᵥ ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>K : Type u_5<VAR>VAdd K β<VAR>k : K<VAR>f : MeasureTheory.SimpleFunc α β<VAR>a : α<GOAL>↑(k +ᵥ f) a = k +ᵥ ↑f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>K : Type u_5<VAR>SMul K β<VAR>k : K<VAR>f : MeasureTheory.SimpleFunc α β<VAR>a : α<GOAL>↑(k • f) a = k • ↑f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Monoid β<VAR>f : MeasureTheory.SimpleFunc α β<VAR>n : ℕ<GOAL>↑(f ^ n) = ↑f ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Monoid β<VAR>n : ℕ<VAR>f : MeasureTheory.SimpleFunc α β<VAR>a : α<GOAL>↑(f ^ n) a = ↑f a ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>DivInvMonoid β<VAR>f : MeasureTheory.SimpleFunc α β<VAR>z : ℤ<GOAL>↑(f ^ z) = ↑f ^ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>DivInvMonoid β<VAR>z : ℤ<VAR>f : MeasureTheory.SimpleFunc α β<VAR>a : α<GOAL>↑(f ^ z) a = ↑f a ^ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>K : Type u_5<VAR>SMul K β<VAR>k : K<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>k • f = MeasureTheory.SimpleFunc.map (fun x => k • x) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>f : γ → MeasureTheory.SimpleFunc α β<VAR>s : Finset γ<VAR>a : α<GOAL>↑(s.sup f) a = s.sup fun c => ↑(f c) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Zero β<VAR>f : MeasureTheory.SimpleFunc α β<VAR>s : Set α<VAR>hs : ¬MeasurableSet s<GOAL>f.restrict s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Zero β<VAR>f : MeasureTheory.SimpleFunc α β<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>↑(f.restrict s) = s.indicator ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Zero β<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>f.restrict Set.univ = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Zero β<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>f.restrict ∅ = 0