ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ.withDensity (s.indicator 1) = μ.restrict s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : Measurable f<GOAL>(μ.withDensity fun x => ENNReal.ofReal (f x)).MutuallySingular (μ.withDensity fun x => ENNReal.ofReal (-f x))
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f : α → ℝ≥0∞<GOAL>(μ.withDensity f).restrict s = (μ.restrict s).withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>s : Set α<VAR>f : α → ℝ≥0∞<GOAL>(μ.withDensity f).restrict s = (μ.restrict s).withDensity f
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>(μ.withDensity f).trim hm = (μ.trim hm).withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>h : μ.MutuallySingular ν<GOAL>(μ.withDensity f).MutuallySingular ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>μ.withDensity f = 0 ↔ f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hf : AEMeasurable f μ<GOAL>(μ.withDensity f) s = 0 ↔ μ ({x | f x ≠ 0} ∩ s) = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hf : Measurable f<GOAL>(μ.withDensity f) s = 0 ↔ μ ({x | f x ≠ 0} ∩ s) = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : α → Prop<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>(∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : α → Prop<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>(∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : α → Prop<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>(∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ.restrict {x | f x ≠ 0}, p x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : α → Prop<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>(∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ.restrict {x | f x ≠ 0}, p x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0<VAR>hf : AEMeasurable f μ<VAR>g : α → ℝ≥0∞<GOAL>AEMeasurable g (μ.withDensity fun x => ↑(f x)) ↔ AEMeasurable (fun x => ↑(f x) * g x) μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0<VAR>hf : Measurable f<VAR>g : α → ℝ≥0∞<GOAL>AEMeasurable g (μ.withDensity fun x => ↑(f x)) ↔ AEMeasurable (fun x => ↑(f x) * g x) μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>h_mf : Measurable f<VAR>g : α → ℝ≥0∞<GOAL>Measurable g → ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : α) in s, g x ∂μ.withDensity f = ∫⁻ (x : α) in s, (f * g) x ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>g : α → ℝ≥0∞<VAR>hg : AEMeasurable g (μ.withDensity f)<GOAL>∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>g : α → ℝ≥0∞<VAR>hg : AEMeasurable g (μ.withDensity f)<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>g : α → ℝ≥0∞<VAR>hg : AEMeasurable g μ<GOAL>∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>g : α → ℝ≥0∞<VAR>hg : AEMeasurable g μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>f_meas : Measurable f<VAR>g : α → ℝ≥0∞<GOAL>∫⁻ (a : α), g a ∂μ.withDensity f ≤ ∫⁻ (a : α), (f * g) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>f_meas : Measurable f<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g : α → ℝ≥0∞<GOAL>∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>f_meas : Measurable f<VAR>g : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : ∀ᵐ (x : α) ∂μ.restrict s, f x < ⊤<GOAL>∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g : α → ℝ≥0∞<GOAL>∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>g : α → ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ⊤<GOAL>∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>g : α → ℝ≥0∞<VAR>h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ⊤<GOAL>∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>μ.withDensity (f * g) = (μ.withDensity f).withDensity g
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>μ.withDensity (f * g) = (μ.withDensity f).withDensity g
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>(μ.withDensity f).withDensity f⁻¹ ≤ μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<GOAL>((μ.withDensity f).withDensity fun x => (f x)⁻¹) = μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<GOAL>((μ.withDensity f).withDensity fun x => (f x)⁻¹) = μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0<GOAL>μ.AbsolutelyContinuous (μ.withDensity f)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type<VAR>f g : α → β<VAR>d : α → ℝ≥0∞<VAR>hd : AEMeasurable d μ<VAR>h_ae_nonneg : ∀ᵐ (x : α) ∂μ, d x ≠ 0<GOAL>f =ᵐ[μ.withDensity d] g ↔ f =ᵐ[μ] g
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>f : α → ℝ≥0∞<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<GOAL>MeasureTheory.SigmaFinite (μ.withDensity f)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>f : α → ℝ≥0∞<VAR>hf_ne_top : ∀ (x : α), f x ≠ ⊤<GOAL>MeasureTheory.SigmaFinite (μ.withDensity f)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>f : α → ℝ≥0∞<GOAL>∃ g, Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>f : α → ℝ≥0∞<VAR>_hf : Measurable f<GOAL>MeasureTheory.SFinite (μ.withDensity f)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>f : α → ℝ≥0∞<VAR>_hf : Measurable f<GOAL>MeasureTheory.SFinite (μ.withDensity f)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>f : α → ℝ≥0<VAR>hf : Continuous f<GOAL>MeasureTheory.IsLocallyFiniteMeasure (μ.withDensity fun x => ↑(f x))
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>f : α → ℝ<VAR>hf : Continuous f<GOAL>MeasureTheory.IsLocallyFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>LinearOrder α<VAR>a b : α<VAR>P : α → Prop<GOAL>(∀ᵐ (x : α) ∂μ, x ∈ Ι a b → P x) ↔ (∀ᵐ (x : α) ∂μ, x ∈ Set.Ioc a b → P x) ∧ ∀ᵐ (x : α) ∂μ, x ∈ Set.Ioc b a → P x
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s₁ s₂ : Set α<VAR>hd : Disjoint s₁ s₂<VAR>h : MeasurableSet s₂<GOAL>μ (s₁ ∪ s₂) = μ s₁ + μ s₂
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s₁ s₂ : Set α<VAR>hd : Disjoint s₁ s₂<VAR>h : MeasurableSet s₁<GOAL>μ (s₁ ∪ s₂) = μ s₁ + μ s₂
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>t : Set α<VAR>s : Set α<VAR>ht : MeasurableSet t<GOAL>μ (s ∩ t) + μ (s \ t) = μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>t : Set α<VAR>s : Set α<VAR>ht : MeasurableSet t<GOAL>μ (s \ t) + μ (s ∩ t) = μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>t : Set α<VAR>s : Set α<VAR>ht : MeasurableSet t<GOAL>μ (s ∪ t) + μ (s ∩ t) = μ s + μ t
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<GOAL>μ (s ∪ t) + μ (s ∩ t) = μ s + μ t
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>μ (symmDiff s t) = μ (s \ t) + μ (t \ s)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t u : Set α<GOAL>μ (symmDiff s u) ≤ μ (symmDiff s t) + μ (symmDiff t u)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : MeasurableSet s<GOAL>μ s + μ sᶜ = μ Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set β<VAR>f : β → Set α<VAR>hs : s.Countable<VAR>hd : s.Pairwise (MeasureTheory.AEDisjoint μ on f)<VAR>h : ∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ<GOAL>μ (⋃ b ∈ s, f b) = ∑' (p : ↑s), μ (f ↑p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set β<VAR>f : β → Set α<VAR>hs : s.Countable<VAR>hd : s.PairwiseDisjoint f<VAR>h : ∀ b ∈ s, MeasurableSet (f b)<GOAL>μ (⋃ b ∈ s, f b) = ∑' (p : ↑s), μ (f ↑p)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>S : Set (Set α)<VAR>hs : S.Countable<VAR>hd : S.Pairwise (MeasureTheory.AEDisjoint μ)<VAR>h : ∀ s ∈ S, MeasureTheory.NullMeasurableSet s μ<GOAL>μ (⋃₀ S) = ∑' (s : ↑S), μ ↑s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>S : Set (Set α)<VAR>hs : S.Countable<VAR>hd : S.Pairwise Disjoint<VAR>h : ∀ s ∈ S, MeasurableSet s<GOAL>μ (⋃₀ S) = ∑' (s : ↑S), μ ↑s
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Finset ι<VAR>f : ι → Set α<VAR>hd : (↑s).Pairwise (MeasureTheory.AEDisjoint μ on f)<VAR>hm : ∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ<GOAL>μ (⋃ b ∈ s, f b) = ∑ p ∈ s, μ (f p)
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Finset ι<VAR>f : ι → Set α<VAR>hd : (↑s).PairwiseDisjoint f<VAR>hm : ∀ b ∈ s, MeasurableSet (f b)<GOAL>μ (⋃ b ∈ s, f b) = ∑ p ∈ s, μ (f p)
<VAR>α : Type u_1<VAR>ι : Type u_8<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ<VAR>As_disj : Pairwise (MeasureTheory.AEDisjoint μ on As)<GOAL>∑' (i : ι), μ (As i) ≤ μ (⋃ i, As i)
<VAR>α : Type u_1<VAR>ι : Type u_8<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), MeasurableSet (As i)<VAR>As_disj : Pairwise (Disjoint on As)<GOAL>∑' (i : ι), μ (As i) ≤ μ (⋃ i, As i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set β<VAR>hs : s.Countable<VAR>f : α → β<VAR>hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})<GOAL>∑' (b : ↑s), μ (f ⁻¹' {↑b}) = μ (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set β<VAR>f : α → β<VAR>hs : s.Countable<GOAL>μ (f ⁻¹' s) = 0 ↔ ∀ x ∈ s, μ (f ⁻¹' {x}) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Finset β<VAR>f : α → β<VAR>hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})<GOAL>∑ b ∈ s, μ (f ⁻¹' {b}) = μ (f ⁻¹' ↑s)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s₁ s₂ : Set α<VAR>h : μ (s₁ ∩ s₂) = 0<GOAL>μ (s₁ \ s₂) = μ s₁
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<GOAL>μ s + μ (t \ s) = μ (s ∪ t)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>t : Set α<VAR>s : Set α<VAR>hm : MeasurableSet t<VAR>h_fin : μ t ≠ ⊤<GOAL>μ (s \ t) = μ (s ∪ t) - μ t
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s₁ s₂ : Set α<VAR>h : s₂ ⊆ s₁<VAR>h₂ : MeasurableSet s₂<VAR>h_fin : μ s₂ ≠ ⊤<GOAL>μ (s₁ \ s₂) = μ s₁ - μ s₂
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s₁ s₂ : Set α<GOAL>μ s₁ - μ s₂ ≤ μ (s₁ \ s₂)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hμst : μ (symmDiff s t) ≠ ⊤<GOAL>μ s = ⊤ ↔ μ t = ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hμst : μ (symmDiff s t) ≠ ⊤<GOAL>μ s ≠ ⊤ ↔ μ t ≠ ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>hst : s ⊆ t<VAR>hs' : μ s ≠ ⊤<VAR>ε : ENNReal<VAR>h : μ t < μ s + ε<GOAL>μ (t \ s) < ε
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>hst : s ⊆ t<VAR>hs' : μ s ≠ ⊤<VAR>ε : ENNReal<GOAL>μ (t \ s) ≤ ε ↔ μ t ≤ μ s + ε
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>h_nulldiff : μ (t \ s) = 0<GOAL>μ s = μ t
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s₁ s₂ s₃ : Set α<VAR>h12 : s₁ ⊆ s₂<VAR>h23 : s₂ ⊆ s₃<VAR>h_nulldiff : μ (s₃ \ s₁) = 0<GOAL>μ s₁ = μ s₂ ∧ μ s₂ = μ s₃
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s₁ s₂ s₃ : Set α<VAR>h12 : s₁ ⊆ s₂<VAR>h23 : s₂ ⊆ s₃<VAR>h_nulldiff : μ (s₃ \ s₁) = 0<GOAL>μ s₁ = μ s₂
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s₁ s₂ s₃ : Set α<VAR>h12 : s₁ ⊆ s₂<VAR>h23 : s₂ ⊆ s₃<VAR>h_nulldiff : μ (s₃ \ s₁) = 0<GOAL>μ s₂ = μ s₃
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : MeasureTheory.NullMeasurableSet s μ<VAR>hs : μ s ≠ ⊤<GOAL>μ sᶜ = μ Set.univ - μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h₁ : MeasurableSet s<VAR>h_fin : μ s ≠ ⊤<GOAL>μ sᶜ = μ Set.univ - μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>ht : μ (s \ t) = 0<GOAL>μ (s ∩ t) = μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>ht : μ tᶜ = 0<GOAL>μ (s ∩ t) = μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<GOAL>s ∪ t =ᵐ[μ] s ↔ t ≤ᵐ[μ] s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<GOAL>s ∪ t =ᵐ[μ] t ↔ s ≤ᵐ[μ] t
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h₁ : s ≤ᵐ[μ] t<VAR>h₂ : μ t ≤ μ s<VAR>hsm : MeasurableSet s<VAR>ht : μ t ≠ ⊤<GOAL>s =ᵐ[μ] t
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h₁ : s ⊆ t<VAR>h₂ : μ t ≤ μ s<VAR>hsm : MeasurableSet s<VAR>ht : μ t ≠ ⊤<GOAL>s =ᵐ[μ] t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable β<VAR>s t : β → Set α<VAR>hsub : ∀ (b : β), s b ⊆ t b<VAR>h_le : ∀ (b : β), μ (t b) ≤ μ (s b)<GOAL>μ (⋃ b, s b) = μ (⋃ b, t b)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s₁ s₂ t₁ t₂ : Set α<VAR>hs : s₁ ⊆ s₂<VAR>hsμ : μ s₂ ≤ μ s₁<VAR>ht : t₁ ⊆ t₂<VAR>htμ : μ t₂ ≤ μ t₁<GOAL>μ (s₁ ∪ t₁) = μ (s₂ ∪ t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable β<VAR>s : β → Set α<GOAL>μ (⋃ b, MeasureTheory.toMeasurable μ (s b)) = μ (⋃ b, s b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>I : Set β<VAR>hc : I.Countable<VAR>s : β → Set α<GOAL>μ (⋃ b ∈ I, MeasureTheory.toMeasurable μ (s b)) = μ (⋃ b ∈ I, s b)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<GOAL>μ (MeasureTheory.toMeasurable μ s ∪ t) = μ (s ∪ t)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<GOAL>μ (s ∪ MeasureTheory.toMeasurable μ t) = μ (s ∪ t)
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Finset ι<VAR>t : ι → Set α<VAR>h : ∀ i ∈ s, MeasureTheory.NullMeasurableSet (t i) μ<VAR>H : (↑s).Pairwise (MeasureTheory.AEDisjoint μ on t)<GOAL>∑ i ∈ s, μ (t i) ≤ μ Set.univ
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ<VAR>H : Pairwise (MeasureTheory.AEDisjoint μ on s)<GOAL>∑' (i : ι), μ (s i) ≤ μ Set.univ
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ<VAR>H : μ Set.univ < ∑' (i : ι), μ (s i)<GOAL>∃ i j, i ≠ j ∧ (s i ∩ s j).Nonempty
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Finset ι<VAR>t : ι → Set α<VAR>h : ∀ i ∈ s, MeasureTheory.NullMeasurableSet (t i) μ<VAR>H : μ Set.univ < ∑ i ∈ s, μ (t i)<GOAL>∃ i ∈ s, ∃ j ∈ s, ∃ (_ : i ≠ j), (t i ∩ t j).Nonempty
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t u : Set α<VAR>ht : MeasurableSet t<VAR>h's : s ⊆ u<VAR>h't : t ⊆ u<VAR>h : μ u < μ s + μ t<GOAL>(s ∩ t).Nonempty
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t u : Set α<VAR>hs : MeasurableSet s<VAR>h's : s ⊆ u<VAR>h't : t ⊆ u<VAR>h : μ u < μ s + μ t<GOAL>(s ∩ t).Nonempty
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<VAR>hd : Directed (fun x x_1 => x ⊆ x_1) s<GOAL>μ (⋃ i, s i) = ⨆ i, μ (s i)
<VAR>α : Type u_8<VAR>ι : Type u_9<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>Preorder ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>f : ι → Set α<GOAL>μ (⋃ i, f i) = ⨆ i, μ (Set.Accumulate f i)
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : ι → Set α<VAR>t : Set ι<VAR>ht : t.Countable<VAR>hd : DirectedOn ((fun x x_1 => x ⊆ x_1) on s) t<GOAL>μ (⋃ i ∈ t, s i) = ⨆ i ∈ t, μ (s i)
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), MeasurableSet (s i)<VAR>hd : Directed (fun x x_1 => x ⊇ x_1) s<VAR>hfin : ∃ i, μ (s i) ≠ ⊤<GOAL>μ (⋂ i, s i) = ⨅ i, μ (s i)
<VAR>α : Type u_8<VAR>ι : Type u_9<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>Preorder ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>f : ι → Set α<VAR>h : ∀ (i : ι), MeasurableSet (f i)<VAR>hfin : ∃ i, μ (f i) ≠ ⊤<GOAL>μ (⋂ i, f i) = ⨅ i, μ (⋂ j, ⋂ (_ : j ≤ i), f j)
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Preorder ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>Countable ι<VAR>s : ι → Set α<VAR>hm : Monotone s<GOAL>Filter.Tendsto (⇑μ ∘ s) Filter.atTop (nhds (μ (⋃ n, s n)))
<VAR>α : Type u_8<VAR>ι : Type u_9<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>Preorder ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>f : ι → Set α<GOAL>Filter.Tendsto (fun i => μ (Set.Accumulate f i)) Filter.atTop (nhds (μ (⋃ i, f i)))
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>Preorder ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), MeasurableSet (s n)<VAR>hm : Antitone s<VAR>hf : ∃ i, μ (s i) ≠ ⊤<GOAL>Filter.Tendsto (⇑μ ∘ s) Filter.atTop (nhds (μ (⋂ n, s n)))
<VAR>α : Type u_8<VAR>ι : Type u_9<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>Preorder ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>f : ι → Set α<VAR>hm : ∀ (i : ι), MeasurableSet (f i)<VAR>hf : ∃ i, μ (f i) ≠ ⊤<GOAL>Filter.Tendsto (fun i => μ (⋂ j ∈ {j | j ≤ i}, f j)) Filter.atTop (nhds (μ (⋂ i, f i)))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_8<VAR>LinearOrder ι<VAR>TopologicalSpace ι<VAR>OrderTopology ι<VAR>DenselyOrdered ι<VAR>FirstCountableTopology ι<VAR>s : ι → Set α<VAR>a : ι<VAR>hs : ∀ r > a, MeasurableSet (s r)<VAR>hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j<VAR>hf : ∃ r > a, μ (s r) ≠ ⊤<GOAL>Filter.Tendsto (⇑μ ∘ s) (nhdsWithin a (Set.Ioi a)) (nhds (μ (⋂ r, ⋂ (_ : r > a), s r)))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : ℕ → Set α<VAR>hs : ∑' (i : ℕ), μ (s i) ≠ ⊤<GOAL>μ (Filter.limsup s Filter.atTop) = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : ℕ → Set α<VAR>h : ∑' (i : ℕ), μ (s i) ≠ ⊤<GOAL>μ (Filter.liminf s Filter.atTop) = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : ℕ → Set α<VAR>t : Set α<VAR>h : ∀ (n : ℕ), s n =ᵐ[μ] t<GOAL>Filter.limsup s Filter.atTop =ᵐ[μ] t
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : ℕ → Set α<VAR>t : Set α<VAR>h : ∀ (n : ℕ), s n =ᵐ[μ] t<GOAL>Filter.liminf s Filter.atTop =ᵐ[μ] t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>x : β<VAR>t : Set β<VAR>s : Set α<GOAL>μ (if x ∈ t then s else ∅) = t.indicator (fun x => μ s) x
<VAR>α : Type u_1<VAR>ms : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>ms ≤ μ.caratheodory
<VAR>α : Type u_1<VAR>ms : MeasurableSpace α<VAR>m : MeasureTheory.OuterMeasure α<VAR>h : ms ≤ m.caratheodory<GOAL>(m.toMeasure h).toOuterMeasure = m.trim
<VAR>α : Type u_1<VAR>ms : MeasurableSpace α<VAR>m : MeasureTheory.OuterMeasure α<VAR>h : ms ≤ m.caratheodory<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(m.toMeasure h) s = m s
<VAR>α : Type u_1<VAR>ms : MeasurableSpace α<VAR>m : MeasureTheory.OuterMeasure α<VAR>h : ms ≤ m.caratheodory<VAR>s : Set α<GOAL>m s ≤ (m.toMeasure h) s
<VAR>α : Type u_1<VAR>ms : MeasurableSpace α<VAR>m : MeasureTheory.OuterMeasure α<VAR>h : ms ≤ m.caratheodory<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s (m.toMeasure h)<GOAL>(m.toMeasure h) s = m s
<VAR>α : Type u_1<VAR>ms : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ.toMeasure ⋯ = μ