ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → F'<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>μ[f + g|m] =ᵐ[μ] μ[f|m] + μ[g|m]
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>f : ι → α → F'<VAR>hf : ∀ i ∈ s, MeasureTheory.Integrable (f i) μ<GOAL>μ[∑ i ∈ s, f i|m] =ᵐ[μ] ∑ i ∈ s, μ[f i|m]
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>c : 𝕜<VAR>f : α → F'<GOAL>μ[c • f|m] =ᵐ[μ] c • μ[f|m]
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → F'<GOAL>μ[-f|m] =ᵐ[μ] -μ[f|m]
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → F'<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>μ[f - g|m] =ᵐ[μ] μ[f|m] - μ[g|m]
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>f : α → F'<VAR>m₁ m₂ m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm₁₂ : m₁ ≤ m₂<VAR>hm₂ : m₂ ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm₂)<GOAL>μ[μ[f|m₂]|m₁] =ᵐ[μ] μ[f|m₁]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedLatticeAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>OrderedSMul ℝ E<VAR>f g : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<VAR>hfg : f ≤ᵐ[μ] g<GOAL>μ[f|m] ≤ᵐ[μ] μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedLatticeAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>OrderedSMul ℝ E<VAR>f : α → E<VAR>hf : 0 ≤ᵐ[μ] f<GOAL>0 ≤ᵐ[μ] μ[f|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedLatticeAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>OrderedSMul ℝ E<VAR>f : α → E<VAR>hf : f ≤ᵐ[μ] 0<GOAL>μ[f|m] ≤ᵐ[μ] 0
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>fs : ℕ → α → F'<VAR>f : α → F'<VAR>bound_fs : α → ℝ<VAR>hfs_meas : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fs n) μ<VAR>h_int_bound_fs : MeasureTheory.Integrable bound_fs μ<VAR>hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x<VAR>hfs : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => fs n x) Filter.atTop (𝓝 (f x))<GOAL>Filter.Tendsto (fun n => MeasureTheory.condexpL1 hm μ (fs n)) Filter.atTop (𝓝 (MeasureTheory.condexpL1 hm μ f))
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>fs gs : ℕ → α → F'<VAR>f g : α → F'<VAR>hfs_int : ∀ (n : ℕ), MeasureTheory.Integrable (fs n) μ<VAR>hgs_int : ∀ (n : ℕ), MeasureTheory.Integrable (gs n) μ<VAR>hfs : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => fs n x) Filter.atTop (𝓝 (f x))<VAR>hgs : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => gs n x) Filter.atTop (𝓝 (g x))<VAR>bound_fs : α → ℝ<VAR>h_int_bound_fs : MeasureTheory.Integrable bound_fs μ<VAR>bound_gs : α → ℝ<VAR>h_int_bound_gs : MeasureTheory.Integrable bound_gs μ<VAR>hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x<VAR>hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x<VAR>hfg : ∀ (n : ℕ), μ[fs n|m] =ᵐ[μ] μ[gs n|m]<GOAL>μ[f|m] =ᵐ[μ] μ[g|m]
<VAR>α : Type u_7<VAR>self : MeasurableSpace α<VAR>f : ℕ → Set α<GOAL>(∀ (i : ℕ), self.MeasurableSet' (f i)) → self.MeasurableSet' (⋃ i, f i)
<VAR>α : Type u_7<VAR>self : MeasurableSpace α<VAR>s : Set α<GOAL>self.MeasurableSet' s → self.MeasurableSet' sᶜ
<VAR>α : Type u_7<VAR>self : MeasurableSpace α<GOAL>self.MeasurableSet' ∅
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>MeasurableSet ∅
<VAR>α : Type u_1<VAR>s : Set α<VAR>m : MeasurableSpace α<GOAL>MeasurableSet s → MeasurableSet sᶜ
<VAR>α : Type u_1<VAR>s : Set α<VAR>m : MeasurableSpace α<VAR>h : MeasurableSet sᶜ<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>s : Set α<VAR>m : MeasurableSpace α<GOAL>MeasurableSet sᶜ ↔ MeasurableSet s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<GOAL>MeasurableSet Set.univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>Subsingleton α<VAR>s : Set α<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>h : s = t<GOAL>MeasurableSet t
<VAR>α : Type u_1<VAR>ι : Sort u_6<VAR>m : MeasurableSpace α<VAR>Countable ι<VAR>f : ι → Set α<VAR>h : ∀ (b : ι), MeasurableSet (f b)<GOAL>MeasurableSet (⋃ b, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>f : β → Set α<VAR>s : Set β<VAR>hs : s.Countable<VAR>h : ∀ b ∈ s, MeasurableSet (f b)<GOAL>MeasurableSet (⋃ b ∈ s, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>f : β → Set α<VAR>s : Set β<VAR>hs : s.Finite<VAR>h : ∀ b ∈ s, MeasurableSet (f b)<GOAL>MeasurableSet (⋃ b ∈ s, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>f : β → Set α<VAR>s : Finset β<VAR>h : ∀ b ∈ s, MeasurableSet (f b)<GOAL>MeasurableSet (⋃ b ∈ s, f b)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : Set (Set α)<VAR>hs : s.Countable<VAR>h : ∀ t ∈ s, MeasurableSet t<GOAL>MeasurableSet (⋃₀ s)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : Set (Set α)<VAR>hs : s.Finite<VAR>h : ∀ t ∈ s, MeasurableSet t<GOAL>MeasurableSet (⋃₀ s)
<VAR>α : Type u_1<VAR>ι : Sort u_6<VAR>m : MeasurableSpace α<VAR>Countable ι<VAR>f : ι → Set α<VAR>h : ∀ (b : ι), MeasurableSet (f b)<GOAL>MeasurableSet (⋂ b, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>f : β → Set α<VAR>s : Set β<VAR>hs : s.Countable<VAR>h : ∀ b ∈ s, MeasurableSet (f b)<GOAL>MeasurableSet (⋂ b ∈ s, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>f : β → Set α<VAR>s : Set β<VAR>hs : s.Finite<VAR>h : ∀ b ∈ s, MeasurableSet (f b)<GOAL>MeasurableSet (⋂ b ∈ s, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>f : β → Set α<VAR>s : Finset β<VAR>h : ∀ b ∈ s, MeasurableSet (f b)<GOAL>MeasurableSet (⋂ b ∈ s, f b)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : Set (Set α)<VAR>hs : s.Countable<VAR>h : ∀ t ∈ s, MeasurableSet t<GOAL>MeasurableSet (⋂₀ s)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : Set (Set α)<VAR>hs : s.Finite<VAR>h : ∀ t ∈ s, MeasurableSet t<GOAL>MeasurableSet (⋂₀ s)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>h₂ : MeasurableSet s₂<GOAL>MeasurableSet (s₁ ∪ s₂)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>h₂ : MeasurableSet s₂<GOAL>MeasurableSet (s₁ ∩ s₂)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>h₂ : MeasurableSet s₂<GOAL>MeasurableSet (s₁ \ s₂)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>h₂ : MeasurableSet s₂<GOAL>MeasurableSet (s₁ ⇨ s₂)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>h₂ : MeasurableSet s₂<GOAL>MeasurableSet (symmDiff s₁ s₂)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>h₂ : MeasurableSet s₂<GOAL>MeasurableSet (bihimp s₁ s₂)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>t s₁ s₂ : Set α<VAR>ht : MeasurableSet t<VAR>h₁ : MeasurableSet s₁<VAR>h₂ : MeasurableSet s₂<GOAL>MeasurableSet (t.ite s₁ s₂)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s t : Set α<VAR>p : Prop<VAR>hs : p → MeasurableSet s<VAR>ht : ¬p → MeasurableSet t<GOAL>MeasurableSet (if p then s else t)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>h₂ : MeasurableSet s₂<VAR>i : Bool<GOAL>MeasurableSet (bif i then s₁ else s₂)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : ℕ → Set α<VAR>h : ∀ (i : ℕ), MeasurableSet (f i)<VAR>n : ℕ<GOAL>MeasurableSet (disjointed f n)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>p : Prop<GOAL>MeasurableSet {_a | p}
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : Set α<GOAL>Nonempty { t // s ⊆ t ∧ MeasurableSet t }
<VAR>α : Type u_1<GOAL>Function.Injective (@MeasurableSet α)
<VAR>α : Type u_1<VAR>m₁ m₂ : MeasurableSpace α<VAR>h : ∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s<GOAL>m₁ = m₂
<VAR>α : Type u_1<VAR>m₁ m₂ : MeasurableSpace α<GOAL>m₁ = m₂ ↔ ∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s
<VAR>α : Type u_7<VAR>MeasurableSpace α<VAR>self : MeasurableSingletonClass α<VAR>x : α<GOAL>MeasurableSet {x}
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>a : α<GOAL>MeasurableSet {a}
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>a : α<GOAL>MeasurableSet {x | x = a}
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>a : α<GOAL>MeasurableSet (insert a s)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>a : α<VAR>s : Set α<GOAL>MeasurableSet (insert a s) ↔ MeasurableSet s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>s : Finset α<GOAL>MeasurableSet ↑s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>s : Set α<VAR>hs : s.Countable<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>p : Set α → Prop<VAR>h : ∀ (s : Set α), p s ↔ MeasurableSet s<VAR>s : Set α<GOAL>MeasurableSet s ↔ p s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>p : Set α → Prop<VAR>h : ∀ (s : Set α), p s ↔ MeasurableSet s<GOAL>m.copy p h = m
<VAR>α : Type u_7<VAR>a b : MeasurableSpace α<GOAL>a ≤ b ↔ a.MeasurableSet' ≤ b.MeasurableSet'
<VAR>α : Type u_1<VAR>s : Set (Set α)<VAR>t : Set α<VAR>ht : t ∈ s<GOAL>MeasurableSet t
<VAR>α : Type u_1<VAR>p : Set α → Prop<VAR>C : Set (Set α)<VAR>hC : ∀ t ∈ C, p t<VAR>h_empty : p ∅<VAR>h_compl : ∀ (t : Set α), p t → p tᶜ<VAR>h_Union : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n)) → p (⋃ i, f i)<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>p s
<VAR>α : Type u_1<VAR>s : Set (Set α)<VAR>m : MeasurableSpace α<VAR>h : ∀ t ∈ s, MeasurableSet t<GOAL>MeasurableSpace.generateFrom s ≤ m
<VAR>α : Type u_1<VAR>s : Set (Set α)<VAR>m : MeasurableSpace α<GOAL>MeasurableSpace.generateFrom s ≤ m ↔ s ⊆ {t | MeasurableSet t}
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>MeasurableSpace.generateFrom {s | MeasurableSet s} = inst✝
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>x y : α<GOAL>(∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) ↔ ∀ s ∈ S, x ∈ s ↔ y ∈ s
<VAR>α : Type u_1<VAR>s : Set (Set α)<VAR>hs : {t | MeasurableSet t} = s<GOAL>MeasurableSpace.mkOfClosure s hs = MeasurableSpace.generateFrom s
<VAR>α : Type u_1<VAR>s t : Set (Set α)<VAR>h : s ⊆ t<GOAL>MeasurableSpace.generateFrom s ≤ MeasurableSpace.generateFrom t
<VAR>α : Type u_1<VAR>s t : Set (Set α)<GOAL>MeasurableSpace.generateFrom s ⊔ MeasurableSpace.generateFrom t = MeasurableSpace.generateFrom (s ∪ t)
<VAR>α : Type u_1<VAR>ι : Sort u_6<VAR>s : ι → Set (Set α)<GOAL>⨆ i, MeasurableSpace.generateFrom (s i) = MeasurableSpace.generateFrom (⋃ i, s i)
<VAR>α : Type u_1<GOAL>MeasurableSpace.generateFrom ∅ = ⊥
<VAR>α : Type u_1<GOAL>MeasurableSpace.generateFrom {∅} = ⊥
<VAR>α : Type u_1<GOAL>MeasurableSpace.generateFrom {Set.univ} = ⊥
<VAR>α : Type u_1<VAR>S : Set (Set α)<GOAL>MeasurableSpace.generateFrom (insert Set.univ S) = MeasurableSpace.generateFrom S
<VAR>α : Type u_1<VAR>S : Set (Set α)<GOAL>MeasurableSpace.generateFrom (insert ∅ S) = MeasurableSpace.generateFrom S
<VAR>α : Type u_1<VAR>s : Set α<GOAL>MeasurableSet s ↔ s = ∅ ∨ s = Set.univ
<VAR>α : Type u_1<VAR>s : Set α<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>m₁ m₂ : MeasurableSpace α<VAR>s : Set α<GOAL>MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
<VAR>α : Type u_1<VAR>ms : Set (MeasurableSpace α)<VAR>s : Set α<GOAL>MeasurableSet s ↔ ∀ m ∈ ms, MeasurableSet s
<VAR>α : Type u_1<VAR>ι : Sort u_7<VAR>m : ι → MeasurableSpace α<VAR>s : Set α<GOAL>MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s
<VAR>α : Type u_1<VAR>m₁ m₂ : MeasurableSpace α<VAR>s : Set α<GOAL>MeasurableSet s ↔ MeasurableSpace.GenerateMeasurable (MeasurableSet ∪ MeasurableSet) s
<VAR>α : Type u_1<VAR>ms : Set (MeasurableSpace α)<VAR>s : Set α<GOAL>MeasurableSet s ↔ MeasurableSpace.GenerateMeasurable {s | ∃ m ∈ ms, MeasurableSet s} s
<VAR>α : Type u_1<VAR>ι : Sort u_7<VAR>m : ι → MeasurableSpace α<VAR>s : Set α<GOAL>MeasurableSet s ↔ MeasurableSpace.GenerateMeasurable {s | ∃ i, MeasurableSet s} s
<VAR>α : Type u_1<VAR>ι : Sort u_6<VAR>m : ι → MeasurableSpace α<GOAL>⨆ n, m n = MeasurableSpace.generateFrom {s | ∃ n, MeasurableSet s}
<VAR>α : Type u_1<VAR>ι : Sort u_6<VAR>m : ι → MeasurableSpace α<GOAL>MeasurableSpace.generateFrom (⋃ n, {t | MeasurableSet t}) = ⨆ n, m n
<VAR>α : Type u_1<GOAL>∀ {x : MeasurableSpace α}, Measurable id
<VAR>α : Type u_1<GOAL>∀ {x : MeasurableSpace α}, Measurable fun a => a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<GOAL>∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace γ} {g : β → γ} {f : α → β}, Measurable g → Measurable f → Measurable (g ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<GOAL>∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace γ} {g : β → γ} {f : α → β}, Measurable g → Measurable f → Measurable fun x => g (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {a : α}, Measurable fun x => a
<VAR>β : Type u_2<VAR>α : Type u_7<VAR>m m0 : MeasurableSpace α<GOAL>∀ {x : MeasurableSpace β}, m ≤ m0 → ∀ {f : α → β}, Measurable f → Measurable f
<VAR>α : Type u_7<VAR>MeasurableSpace α<VAR>self : DiscreteMeasurableSpace α<VAR>s : Set α<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>DiscreteMeasurableSpace α<VAR>s : Set α<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>DiscreteMeasurableSpace α<VAR>f : α → β<GOAL>Measurable f
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>self : MeasurableSpace.CountablyGenerated α<GOAL>∃ b, b.Countable ∧ m = MeasurableSpace.generateFrom b
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>h : MeasurableSpace.CountablyGenerated α<GOAL>(MeasurableSpace.countableGeneratingSet α).Countable
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>h : MeasurableSpace.CountablyGenerated α<GOAL>MeasurableSpace.generateFrom (MeasurableSpace.countableGeneratingSet α) = m
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<GOAL>∅ ∈ MeasurableSpace.countableGeneratingSet α
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<GOAL>(MeasurableSpace.countableGeneratingSet α).Nonempty
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<VAR>s : Set α<VAR>hs : s ∈ MeasurableSpace.countableGeneratingSet α<GOAL>MeasurableSet s
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<GOAL>MeasurableSpace.generateFrom (Set.range (MeasurableSpace.natGeneratingSequence α)) = m
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<GOAL>MeasurableSet (MeasurableSpace.natGeneratingSequence α n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace β<VAR>h : MeasurableSpace.CountablyGenerated β<VAR>f : α → β<GOAL>MeasurableSpace.CountablyGenerated α
<VAR>β : Type u_2<VAR>m₁ m₂ : MeasurableSpace β<VAR>h₁ : MeasurableSpace.CountablyGenerated β<VAR>h₂ : MeasurableSpace.CountablyGenerated β<GOAL>MeasurableSpace.CountablyGenerated β
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>self : MeasurableSpace.SeparatesPoints α<VAR>x y : α<GOAL>(∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s) → x = y
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>hs : MeasurableSpace.SeparatesPoints α<VAR>x y : α<VAR>h : ∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s<GOAL>x = y
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSpace.SeparatesPoints α<VAR>x y : α<VAR>h : x ≠ y<GOAL>∃ s, MeasurableSet s ∧ x ∈ s ∧ y ∉ s
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>MeasurableSpace.SeparatesPoints α ↔ ∀ (x y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>h : MeasurableSpace.SeparatesPoints α<VAR>x y : α<GOAL>(∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
<VAR>α : Type u_1<VAR>m m' : MeasurableSpace α<VAR>hsep : MeasurableSpace.SeparatesPoints α<VAR>h : m ≤ m'<GOAL>MeasurableSpace.SeparatesPoints α
<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>self : MeasurableSpace.CountablySeparated α<GOAL>HasCountableSeparatingOn α MeasurableSet Set.univ
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>MeasurableSpace.CountablySeparated α ↔ HasCountableSeparatingOn α MeasurableSet Set.univ
<VAR>α : Type u_1<VAR>m m' : MeasurableSpace α<VAR>hsep : MeasurableSpace.CountablySeparated α<VAR>h : m ≤ m'<GOAL>MeasurableSpace.CountablySeparated α
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<GOAL>MeasurableSpace.CountablySeparated ↑s ↔ HasCountableSeparatingOn α MeasurableSet s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>h : MeasurableSpace.CountablySeparated α<GOAL>∃ m', MeasurableSpace.CountablyGenerated α ∧ MeasurableSpace.SeparatesPoints α ∧ m' ≤ m
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<GOAL>Measurable (MeasurableSpace.mapNatBool α)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<VAR>MeasurableSpace.SeparatesPoints α<GOAL>Function.Injective (MeasurableSpace.mapNatBool α)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<VAR>MeasurableSpace.SeparatesPoints α<GOAL>∃ s, Nonempty (α ≃ᵐ ↑s)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSpace.CountablySeparated α<GOAL>∃ f, Measurable f ∧ Function.Injective f
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSpace.CountablySeparated α<GOAL>MeasurableSingletonClass α
<VAR>α : Type u_1<VAR>t : ℕ → Set α<VAR>n : ℕ<VAR>s : Set α<VAR>hs : s ∈ memPartition t n<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>t : ℕ → Set α<VAR>n : ℕ<GOAL>MeasurableSpace.generateFrom (memPartition t n) ≤ MeasurableSpace.generateFrom (memPartition t (n + 1))
<VAR>α : Type u_1<VAR>t : ℕ → Set α<VAR>n : ℕ<VAR>s : Set α<GOAL>MeasurableSet s ↔ ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S
<VAR>α : Type u_1<VAR>t : ℕ → Set α<VAR>n : ℕ<GOAL>MeasurableSet (t n)
<VAR>α : Type u_1<VAR>t : ℕ → Set α<GOAL>MeasurableSpace.generateFrom (⋃ n, memPartition t n) = MeasurableSpace.generateFrom (Set.range t)
<VAR>α : Type u_1<VAR>t : ℕ → Set α<VAR>n : ℕ<GOAL>MeasurableSpace.generateFrom (memPartition t n) ≤ MeasurableSpace.generateFrom (Set.range t)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<GOAL>MeasurableSpace.generateFrom (⋃ n, memPartition t n) ≤ m
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<VAR>n : ℕ<GOAL>MeasurableSpace.generateFrom (memPartition t n) ≤ m
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<VAR>n : ℕ<VAR>s : Set α<VAR>hs : s ∈ memPartition t n<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<VAR>n : ℕ<VAR>a : α<GOAL>MeasurableSet (memPartitionSet t n a)
<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<GOAL>MeasurableSet (Set.enumerateCountable ⋯ ∅ n)
<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<GOAL>(MeasurableSpace.countablePartition α n).Finite
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>h : MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<VAR>s t : Set α<VAR>hs : s ∈ MeasurableSpace.countablePartition α n<VAR>ht : t ∈ MeasurableSpace.countablePartition α n<VAR>hst : s ≠ t<GOAL>Disjoint s t
<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<GOAL>⋃₀ MeasurableSpace.countablePartition α n = Set.univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>h : MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<VAR>s : Set α<GOAL>MeasurableSet s ↔ ∃ S, ↑S ⊆ MeasurableSpace.countablePartition α n ∧ s = ⋃₀ ↑S
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>h : MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<VAR>s : Set α<VAR>hs : s ∈ MeasurableSpace.countablePartition α n<GOAL>MeasurableSet s
<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<GOAL>MeasurableSpace.generateFrom (MeasurableSpace.countablePartition α n) ≤ MeasurableSpace.generateFrom (MeasurableSpace.countablePartition α (n + 1))
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<GOAL>MeasurableSpace.generateFrom (⋃ n, MeasurableSpace.countablePartition α n) = m
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<GOAL>MeasurableSpace.generateFrom (MeasurableSpace.countablePartition α n) ≤ m
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>h : MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<VAR>a : α<GOAL>MeasurableSpace.countablePartitionSet n a ∈ MeasurableSpace.countablePartition α n
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>h : MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<VAR>a : α<GOAL>a ∈ MeasurableSpace.countablePartitionSet n a
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>h : MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ MeasurableSpace.countablePartition α n<GOAL>MeasurableSpace.countablePartitionSet n a = s ↔ a ∈ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>h : MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ MeasurableSpace.countablePartition α n<VAR>ha : a ∈ s<GOAL>MeasurableSpace.countablePartitionSet n a = s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>h : MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<VAR>a : α<GOAL>MeasurableSet (MeasurableSpace.countablePartitionSet n a)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>self : MeasurableSpace.CountableOrCountablyGenerated α β<GOAL>Countable α ∨ MeasurableSpace.CountablyGenerated β
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>hμm : MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm) =ᵐ[μ] μ[f|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<GOAL>MeasureTheory.eLpNorm (μ[f|m]) 1 μ ≤ MeasureTheory.eLpNorm f 1 μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<GOAL>∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f : α → ℝ<GOAL>∫ (x : α) in s, |(μ[f|m]) x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>R : ℝ≥0<VAR>f : α → ℝ<VAR>hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R<GOAL>∀ᵐ (x : α) ∂μ, |(μ[f|m]) x| ≤ ↑R
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_2<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>g : α → ℝ<VAR>hint : MeasureTheory.Integrable g μ<VAR>ℱ : ι → MeasurableSpace α<VAR>hℱ : ∀ (i : ι), ℱ i ≤ m0<GOAL>MeasureTheory.UniformIntegrable (fun i => μ[g|ℱ i]) 1 μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : MeasureTheory.SimpleFunc α ℝ<VAR>g : α → ℝ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>μ[↑f * g|m] =ᵐ[μ] ↑f * μ[g|m]