ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>MeasureTheory.SigmaFinite μ<VAR>f g : α → E<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 ∂μ<GOAL>f =ᵐ[μ] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : α → E<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 : MeasureTheory.AEFinStronglyMeasurable f μ<GOAL>f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f g : α → E<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>hf : MeasureTheory.AEFinStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEFinStronglyMeasurable g μ<GOAL>f =ᵐ[μ] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>p : ℝ≥0∞<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<GOAL>↑↑f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>p : ℝ≥0∞<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 ∂μ<GOAL>↑↑f =ᵐ[μ] ↑↑g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>hm : m ≤ m0<VAR>f : α → E<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 : MeasureTheory.FinStronglyMeasurable f (μ.trim hm)<GOAL>f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<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>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f g : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<VAR>hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<GOAL>f =ᵐ[μ] g
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>μ : MeasureTheory.Measure β<VAR>f : β → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>h'f : ∀ (s : Set β), IsClosed s → ∫ (x : β) in s, f x ∂μ = 0<GOAL>f =ᵐ[μ] 0
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>SigmaCompactSpace β<VAR>R1Space β<VAR>μ : MeasureTheory.Measure β<VAR>f : β → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0<GOAL>f =ᵐ[μ] 0
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>SigmaCompactSpace β<VAR>R1Space β<VAR>μ : MeasureTheory.Measure β<VAR>f : β → E<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0<GOAL>f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤<VAR>hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ<GOAL>f =ᵐ[μ] g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>μ.withDensity f = μ.withDensity g ↔ f =ᵐ[μ] g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<GOAL>μ.withDensity f = μ.withDensity g ↔ f =ᵐ[μ] g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<VAR>hd : Pairwise (MeasureTheory.AEDisjoint μ on s)<GOAL>∃ t, (∀ (i : ι), MeasurableSet (t i)) ∧ (∀ (i : ι), μ (t i) = 0) ∧ Pairwise (Disjoint on fun i => s i \ t i)
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : MeasureTheory.AEDisjoint μ s t<GOAL>μ (s ∩ t) = 0
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : MeasureTheory.AEDisjoint μ s t<GOAL>MeasureTheory.AEDisjoint μ t s
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>Symmetric (MeasureTheory.AEDisjoint μ)
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<GOAL>MeasureTheory.AEDisjoint μ s t ↔ MeasureTheory.AEDisjoint μ t s
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : Disjoint s t<GOAL>MeasureTheory.AEDisjoint μ s t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ι → Set α<VAR>hf : Pairwise (Disjoint on f)<GOAL>Pairwise (MeasureTheory.AEDisjoint μ on f)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ι → Set α<VAR>s : Set ι<VAR>hf : s.PairwiseDisjoint f<GOAL>s.Pairwise (MeasureTheory.AEDisjoint μ on f)
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t u v : Set α<VAR>h : MeasureTheory.AEDisjoint μ s t<VAR>hu : u ≤ᵐ[μ] s<VAR>hv : v ≤ᵐ[μ] t<GOAL>MeasureTheory.AEDisjoint μ u v
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t u v : Set α<VAR>h : MeasureTheory.AEDisjoint μ s t<VAR>hu : u ⊆ s<VAR>hv : v ⊆ t<GOAL>MeasureTheory.AEDisjoint μ u v
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t u v : Set α<VAR>h : MeasureTheory.AEDisjoint μ s t<VAR>hu : u =ᵐ[μ] s<VAR>hv : v =ᵐ[μ] t<GOAL>MeasureTheory.AEDisjoint μ u v
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>t : Set α<VAR>Countable ι<VAR>s : ι → Set α<GOAL>MeasureTheory.AEDisjoint μ (⋃ i, s i) t ↔ ∀ (i : ι), MeasureTheory.AEDisjoint μ (s i) t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>Countable ι<VAR>t : ι → Set α<GOAL>MeasureTheory.AEDisjoint μ s (⋃ i, t i) ↔ ∀ (i : ι), MeasureTheory.AEDisjoint μ s (t i)
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t u : Set α<GOAL>MeasureTheory.AEDisjoint μ (s ∪ t) u ↔ MeasureTheory.AEDisjoint μ s u ∧ MeasureTheory.AEDisjoint μ t u
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t u : Set α<GOAL>MeasureTheory.AEDisjoint μ s (t ∪ u) ↔ MeasureTheory.AEDisjoint μ s t ∧ MeasureTheory.AEDisjoint μ s u
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t u : Set α<VAR>hs : MeasureTheory.AEDisjoint μ s u<VAR>ht : MeasureTheory.AEDisjoint μ t u<GOAL>MeasureTheory.AEDisjoint μ (s ∪ t) u
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t u : Set α<VAR>ht : MeasureTheory.AEDisjoint μ s t<VAR>hu : MeasureTheory.AEDisjoint μ s u<GOAL>MeasureTheory.AEDisjoint μ s (t ∪ u)
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : MeasureTheory.AEDisjoint μ s t<GOAL>s \ t =ᵐ[μ] s
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : MeasureTheory.AEDisjoint μ s t<GOAL>t \ s =ᵐ[μ] t
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : MeasureTheory.AEDisjoint μ s t<GOAL>μ (s \ t) = μ s
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : MeasureTheory.AEDisjoint μ s t<GOAL>μ (t \ s) = μ t
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : MeasureTheory.AEDisjoint μ s t<GOAL>∃ u, MeasurableSet u ∧ μ u = 0 ∧ Disjoint (s \ u) t
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : μ t = 0<GOAL>MeasureTheory.AEDisjoint μ s t
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : μ s = 0<GOAL>MeasureTheory.AEDisjoint μ s t
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>MeasureTheory.AEDisjoint μ sᶜ s
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>MeasureTheory.AEDisjoint μ s sᶜ
<VAR>α : Type u_6<VAR>MeasurableSpace α<VAR>self : MeasureTheory.Measure α<GOAL>self.trim ≤ self.toOuterMeasure
<VAR>α : Type u_6<VAR>MeasurableSpace α<VAR>self : MeasureTheory.Measure α<VAR>f : ℕ → Set α<GOAL>(∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → self.toOuterMeasure (⋃ i, f i) = ∑' (i : ℕ), self.toOuterMeasure (f i)
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>Function.Injective MeasureTheory.Measure.toOuterMeasure
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ.trim = μ.toOuterMeasure
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.Measure.ofMeasurable m m0 mU) s = m s hs
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ₁ μ₂ : MeasureTheory.Measure α<VAR>h : ∀ (s : Set α), MeasurableSet s → μ₁ s = μ₂ s<GOAL>μ₁ = μ₂
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ₁ μ₂ : MeasureTheory.Measure α<GOAL>μ₁ = μ₂ ↔ ∀ (s : Set α), MeasurableSet s → μ₁ s = μ₂ s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ₁ μ₂ : MeasureTheory.Measure α<GOAL>μ₁ = μ₂ ↔ ∀ (s : Set α), μ₁ s = μ₂ s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>m : MeasureTheory.OuterMeasure α<GOAL>m ≤ μ.toOuterMeasure ↔ ∀ (s : Set α), MeasurableSet s → m s ≤ μ s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>⇑μ.toOuterMeasure = ⇑μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>μ.toOuterMeasure s = μ s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>μ s = μ.trim s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>μ s = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), μ t
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>μ s = ⨅ t, μ ↑t
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>μ s = (MeasureTheory.inducedOuterMeasure (fun s x => μ s) ⋯ ⋯) s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ.toOuterMeasure = MeasureTheory.inducedOuterMeasure (fun s x => μ s) ⋯ ⋯
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ s = MeasureTheory.extend (fun t _ht => μ t) s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : μ s ≠ 0<GOAL>s.Nonempty
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s₁ s₂ : Set α<VAR>h : s₁ ⊆ s₂<VAR>h₁ : μ s₁ = ⊤<GOAL>μ s₂ = ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<GOAL>μ s ≤ μ (s ∪ t)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<GOAL>μ t ≤ μ (s ∪ t)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = μ s
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>MeasurableSpace α<VAR>Countable ι<VAR>μ : ι → MeasureTheory.Measure α<VAR>s : Set α<GOAL>∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i) s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s : Set α<GOAL>∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = μ s ∧ ν t = ν s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : μ s = 0<GOAL>∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>(∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = 0) ↔ μ s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set β<VAR>f : β → Set α<VAR>hs : s.Finite<VAR>hfin : ∀ i ∈ s, μ (f i) ≠ ⊤<GOAL>μ (⋃ i ∈ s, f i) < ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Prop<VAR>s : ι → Set α<GOAL>μ (⋃ (i : ι), s i) = 0 ↔ ∀ (i : ι), μ (s i) = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : μ s < ⊤<VAR>ht : μ t < ⊤<GOAL>μ (s ∪ t) < ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<GOAL>μ (s ∪ t) < ⊤ ↔ μ s < ⊤ ∧ μ t < ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : μ s ≠ ⊤<VAR>ht : μ t ≠ ⊤<GOAL>μ (s ∪ t) ≠ ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : μ s ≠ ⊤<VAR>ht : μ t ≠ ⊤<GOAL>μ (symmDiff s t) ≠ ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<GOAL>μ (s ∪ t) = ⊤ ↔ μ s = ⊤ ∨ μ t = ⊤
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<VAR>hs : μ (⋃ n, s n) ≠ 0<GOAL>∃ n, 0 < μ (s n)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hst : t ⊆ s<VAR>hs : μ s ≠ ⊤<GOAL>μ t < ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs_finite : μ s ≠ ⊤<GOAL>μ (s ∩ t) < ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>ht_finite : μ t ≠ ⊤<GOAL>μ (s ∩ t) < ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>S : Set α<VAR>T : Set α<VAR>h : μ T = 0<GOAL>μ (S ∩ T) = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>S : Set α<VAR>T : Set α<VAR>h : μ S = 0<GOAL>μ (S ∩ T) = 0
<VAR>α : Type u_1<VAR>β : Type u_6<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure β<VAR>C : β → Set α → Prop<VAR>s : Set (Set α)<VAR>m : MeasurableSpace α<VAR>h_eq : m = MeasurableSpace.generateFrom s<VAR>h_inter : IsPiSystem s<VAR>h_empty : ∀ᵐ (x : β) ∂μ, C x ∅<VAR>h_basic : ∀ᵐ (x : β) ∂μ, ∀ t ∈ s, C x t<VAR>h_compl : ∀ᵐ (x : β) ∂μ, ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ<VAR>h_union : ∀ᵐ (x : β) ∂μ, ∀ (f : ℕ → Set α), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)<GOAL>∀ᵐ (x : β) ∂μ, ∀ ⦃t : Set α⦄, MeasurableSet t → C x t
<VAR>α : Type u_6<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>MeasureTheory.toMeasurable μ s = if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s then h.choose else if h' : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u) then h'.choose else ⋯.choose
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>s ⊆ MeasureTheory.toMeasurable μ s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>s ≤ᵐ[μ] MeasureTheory.toMeasurable μ s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>MeasurableSet (MeasureTheory.toMeasurable μ s)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>μ (MeasureTheory.toMeasurable μ s) = μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>h : Measurable f<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>h : AEMeasurable f μ<GOAL>Measurable (AEMeasurable.mk f h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>h : AEMeasurable f μ<GOAL>f =ᵐ[μ] AEMeasurable.mk f h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f g : α → β<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable f μ<VAR>h : f =ᵐ[μ] g<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f g : α → β<VAR>μ : MeasureTheory.Measure α<VAR>h : f =ᵐ[μ] g<GOAL>AEMeasurable f μ ↔ AEMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>b : β<GOAL>AEMeasurable (fun _a => b) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>AEMeasurable id μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>AEMeasurable (fun x => x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace δ<VAR>f : α → δ<VAR>g : δ → β<VAR>hg : Measurable g<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (g ∘ f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace δ<VAR>f : α → δ<VAR>g : δ → β<VAR>hg : Measurable g<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun x => g (f x)) μ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>self : μ.IsOpenPosMeasure<VAR>U : Set X<GOAL>IsOpen U → U.Nonempty → μ U ≠ 0
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>U : Set X<VAR>hU : IsOpen U<VAR>hne : U.Nonempty<GOAL>μ U ≠ 0
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>U : Set X<VAR>hU : IsOpen U<VAR>hne : U.Nonempty<GOAL>0 < μ U
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>U : Set X<VAR>hU : IsOpen U<GOAL>0 < μ U ↔ U.Nonempty
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>U : Set X<VAR>hU : IsOpen U<GOAL>μ U = 0 ↔ U = ∅
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>s : Set X<VAR>h : (interior s).Nonempty<GOAL>0 < μ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>s : Set X<VAR>x : X<VAR>h : s ∈ 𝓝 x<GOAL>0 < μ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>c : ℝ≥0∞<VAR>h : c ≠ 0<GOAL>(c • μ).IsOpenPosMeasure
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>μ ν : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>h : μ ≪ ν<GOAL>ν.IsOpenPosMeasure
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>μ ν : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>h : μ ≤ ν<GOAL>ν.IsOpenPosMeasure
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>U : Set X<VAR>hU : IsOpen U<GOAL>U =ᵐ[μ] ∅ ↔ U = ∅
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>U : Set X<VAR>hU : IsOpen U<VAR>h₀ : μ U = 0<GOAL>U = ∅
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>F : Set X<VAR>hF : IsClosed F<GOAL>F =ᵐ[μ] Set.univ ↔ F = Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>F : Set X<VAR>OpensMeasurableSpace X<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hF : IsClosed F<GOAL>μ F = μ Set.univ ↔ F = Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>F : Set X<VAR>OpensMeasurableSpace X<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hF : IsClosed F<GOAL>μ F = 1 ↔ F = Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>s : Set X<VAR>hs : μ s = 0<GOAL>interior s = ∅
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>U : Set X<VAR>f g : X → Y<VAR>h : f =ᵐ[μ.restrict U] g<VAR>hU : IsOpen U<VAR>hf : ContinuousOn f U<VAR>hg : ContinuousOn g U<GOAL>Set.EqOn f g U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>f g : X → Y<VAR>h : f =ᵐ[μ] g<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>f = g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>s : Set X<VAR>f g : X → Y<VAR>h : f =ᵐ[μ.restrict s] g<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<VAR>hU : s ⊆ closure (interior s)<GOAL>Set.EqOn f g s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>f g : X → Y<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>f =ᵐ[μ] g ↔ f = g
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>OpensMeasurableSpace X<VAR>Z : Type u_3<VAR>TopologicalSpace Z<VAR>MeasurableSpace Z<VAR>BorelSpace Z<VAR>f : X → Z<VAR>hf : Continuous f<VAR>hf_surj : Function.Surjective f<GOAL>(MeasureTheory.Measure.map f μ).IsOpenPosMeasure
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>LinearOrder X<VAR>OrderTopology X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>NoMaxOrder X<VAR>a : X<GOAL>0 < μ (Set.Ioi a)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>LinearOrder X<VAR>OrderTopology X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>NoMinOrder X<VAR>a : X<GOAL>0 < μ (Set.Iio a)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>LinearOrder X<VAR>OrderTopology X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>DenselyOrdered X<VAR>a b : X<GOAL>0 < μ (Set.Ioo a b) ↔ a < b