ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : Disjoint s t<VAR>hs : MeasurableSet s<GOAL>μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ.restrict s + μ.restrict sᶜ = μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ.restrict sᶜ + μ.restrict s = μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s s' : Set α<GOAL>μ.restrict (s ∪ s') ≤ μ.restrict s + μ.restrict s'
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<VAR>hd : Pairwise (MeasureTheory.AEDisjoint μ on s)<VAR>hm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>(μ.restrict (⋃ i, s i)) t = ∑' (i : ι), (μ.restrict (s i)) t
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<VAR>hd : Pairwise (Disjoint on s)<VAR>hm : ∀ (i : ι), MeasurableSet (s i)<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>(μ.restrict (⋃ i, s i)) t = ∑' (i : ι), (μ.restrict (s i)) t
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<VAR>hd : Directed (fun x x_1 => x ⊆ x_1) s<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>(μ.restrict (⋃ i, s i)) t = ⨆ i, (μ.restrict (s i)) t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.Measure.map f μ).restrict s = MeasureTheory.Measure.map f (μ.restrict (f ⁻¹' s))
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : μ s ≠ ⊤<GOAL>μ.restrict (MeasureTheory.toMeasurable μ s) = μ.restrict s
<VAR>α : Type u_2<VAR>_m0 : MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hs : ∀ᵐ (x : α) ∂μ, x ∈ s<GOAL>μ.restrict s = μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ.restrict s = ν.restrict s ↔ ∀ t ⊆ s, MeasurableSet t → μ t = ν t
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : s ⊆ t<VAR>h : μ.restrict t = ν.restrict t<GOAL>μ.restrict s = ν.restrict s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s t : Set α<GOAL>μ.restrict (s ∪ t) = ν.restrict (s ∪ t) ↔ μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s : Finset ι<VAR>t : ι → Set α<GOAL>μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<GOAL>μ.restrict (⋃ i, s i) = ν.restrict (⋃ i, s i) ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s : Set ι<VAR>t : ι → Set α<VAR>hc : s.Countable<GOAL>μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>S : Set (Set α)<VAR>hc : S.Countable<GOAL>μ.restrict (⋃₀ S) = ν.restrict (⋃₀ S) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s
<VAR>α : Type u_2<VAR>t : Set α<VAR>m0 : MeasurableSpace α<VAR>m : Set (MeasureTheory.Measure α)<VAR>hm : m.Nonempty<VAR>ht : MeasurableSet t<GOAL>(sInf m).restrict t = sInf ((fun μ => μ.restrict t) '' m)
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : μ s ≠ 0<VAR>p : α → Prop<VAR>hp : ∀ᵐ (x : α) ∂μ.restrict s, p x<GOAL>∃ x ∈ s, p x
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<VAR>hs : ⋃ i, s i = Set.univ<GOAL>μ = ν ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>S : Set ι<VAR>s : ι → Set α<VAR>hc : S.Countable<VAR>hs : ⋃ i ∈ S, s i = Set.univ<GOAL>μ = ν ↔ ∀ i ∈ S, μ.restrict (s i) = ν.restrict (s i)
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>S : Set (Set α)<VAR>hc : S.Countable<VAR>hs : ⋃₀ S = Set.univ<GOAL>μ = ν ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>S T : Set (Set α)<VAR>h_gen : m0 = MeasurableSpace.generateFrom S<VAR>hc : T.Countable<VAR>h_inter : IsPiSystem S<VAR>hU : ⋃₀ T = Set.univ<VAR>htop : ∀ t ∈ T, μ t ≠ ⊤<VAR>ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)<VAR>T_eq : ∀ t ∈ T, μ t = ν t<GOAL>μ = ν
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>S T : Set (Set α)<VAR>h_gen : m0 = MeasurableSpace.generateFrom S<VAR>h_inter : IsPiSystem S<VAR>h_sub : T ⊆ S<VAR>hc : T.Countable<VAR>hU : ⋃₀ T = Set.univ<VAR>htop : ∀ s ∈ T, μ s ≠ ⊤<VAR>h_eq : ∀ s ∈ S, μ s = ν s<GOAL>μ = ν
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>C : Set (Set α)<VAR>B : ℕ → Set α<VAR>hA : m0 = MeasurableSpace.generateFrom C<VAR>hC : IsPiSystem C<VAR>h1B : ⋃ i, B i = Set.univ<VAR>h2B : ∀ (i : ℕ), B i ∈ C<VAR>hμB : ∀ (i : ℕ), μ (B i) ≠ ⊤<VAR>h_eq : ∀ s ∈ C, μ s = ν s<GOAL>μ = ν
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ : ι → MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.Measure.sum μ).restrict s = MeasureTheory.Measure.sum fun i => (μ i).restrict s
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>Countable ι<VAR>μ : ι → MeasureTheory.Measure α<VAR>s : Set α<GOAL>(MeasureTheory.Measure.sum μ).restrict s = MeasureTheory.Measure.sum fun i => (μ i).restrict s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : μ ≪ ν<VAR>s : Set α<GOAL>μ.restrict s ≪ ν.restrict s
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<VAR>hd : Pairwise (MeasureTheory.AEDisjoint μ on s)<VAR>hm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ<GOAL>μ.restrict (⋃ i, s i) = MeasureTheory.Measure.sum fun i => μ.restrict (s i)
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<VAR>hd : Pairwise (Disjoint on s)<VAR>hm : ∀ (i : ι), MeasurableSet (s i)<GOAL>μ.restrict (⋃ i, s i) = MeasureTheory.Measure.sum fun i => μ.restrict (s i)
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<GOAL>μ.restrict (⋃ i, s i) ≤ MeasureTheory.Measure.sum fun i => μ.restrict (s i)
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<GOAL>MeasureTheory.ae (μ.restrict (⋃ i, s i)) = ⨆ i, MeasureTheory.ae (μ.restrict (s i))
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<GOAL>MeasureTheory.ae (μ.restrict (s ∪ t)) = MeasureTheory.ae (μ.restrict s) ⊔ MeasureTheory.ae (μ.restrict t)
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : ι → Set α<VAR>t : Set ι<VAR>ht : t.Countable<GOAL>MeasureTheory.ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, MeasureTheory.ae (μ.restrict (s i))
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : ι → Set α<VAR>t : Finset ι<GOAL>MeasureTheory.ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, MeasureTheory.ae (μ.restrict (s i))
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<VAR>p : α → Prop<GOAL>(∀ᵐ (x : α) ∂μ.restrict (⋃ i, s i), p x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ.restrict (s i), p x
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>p : α → Prop<GOAL>(∀ᵐ (x : α) ∂μ.restrict (s ∪ t), p x) ↔ (∀ᵐ (x : α) ∂μ.restrict s, p x) ∧ ∀ᵐ (x : α) ∂μ.restrict t, p x
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : ι → Set α<VAR>t : Set ι<VAR>ht : t.Countable<VAR>p : α → Prop<GOAL>(∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x
<VAR>α : Type u_2<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : ι → Set α<VAR>t : Finset ι<VAR>p : α → Prop<GOAL>(∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x
<VAR>α : Type u_2<VAR>δ : Type u_4<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<VAR>f g : α → δ<GOAL>f =ᵐ[μ.restrict (⋃ i, s i)] g ↔ ∀ (i : ι), f =ᵐ[μ.restrict (s i)] g
<VAR>α : Type u_2<VAR>δ : Type u_4<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : ι → Set α<VAR>t : Set ι<VAR>ht : t.Countable<VAR>f g : α → δ<GOAL>f =ᵐ[μ.restrict (⋃ i ∈ t, s i)] g ↔ ∀ i ∈ t, f =ᵐ[μ.restrict (s i)] g
<VAR>α : Type u_2<VAR>δ : Type u_4<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : ι → Set α<VAR>t : Finset ι<VAR>f g : α → δ<GOAL>f =ᵐ[μ.restrict (⋃ i ∈ t, s i)] g ↔ ∀ i ∈ t, f =ᵐ[μ.restrict (s i)] g
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>LinearOrder α<VAR>a b : α<GOAL>MeasureTheory.ae (μ.restrict (Ι a b)) = MeasureTheory.ae (μ.restrict (Set.Ioc a b)) ⊔ MeasureTheory.ae (μ.restrict (Set.Ioc b a))
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>LinearOrder α<VAR>a b : α<VAR>P : α → Prop<GOAL>(∀ᵐ (x : α) ∂μ.restrict (Ι a b), P x) ↔ (∀ᵐ (x : α) ∂μ.restrict (Set.Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Set.Ioc b a), P x
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>p : α → Prop<VAR>hp : MeasureTheory.NullMeasurableSet {x | p x} (μ.restrict s)<GOAL>(∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>p : α → Prop<VAR>hp : MeasurableSet {x | p x}<GOAL>(∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>p : α → Prop<VAR>h : ∀ᵐ (x : α) ∂μ.restrict s, p x<GOAL>∀ᵐ (x : α) ∂μ, x ∈ s → p x
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>p : α → Prop<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>(∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>p : α → Prop<VAR>hs : MeasurableSet s<GOAL>(∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x
<VAR>α : Type u_2<VAR>δ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → δ<VAR>s : Set α<VAR>hfg : f =ᵐ[μ] g<GOAL>f =ᵐ[μ.restrict s] g
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>∀ᵐ (x : α) ∂μ.restrict s, x ∈ s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : α) ∂μ.restrict s, x ∈ s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>p : α → Prop<VAR>h : ∀ᵐ (x : α) ∂μ, p x<GOAL>∀ᵐ (x : α) ∂μ.restrict s, p x
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>p : α → Prop<VAR>hst : s ⊆ t<VAR>h : ∀ᵐ (x : α) ∂μ.restrict t, p x<GOAL>∀ᵐ (x : α) ∂μ.restrict s, p x
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>t : Set α<VAR>p : α → Prop<VAR>ht : ∀ᵐ (x : α) ∂μ.restrict t, p x<VAR>htc : ∀ᵐ (x : α) ∂μ.restrict tᶜ, p x<GOAL>∀ᵐ (x : α) ∂μ, p x
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hs : MeasurableSet s<GOAL>t ∈ Filter.map f (MeasureTheory.ae (μ.restrict s)) ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : α → Prop<VAR>Monoid R<VAR>DistribMulAction R ℝ≥0∞<VAR>IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>h : ∀ᵐ (x : α) ∂μ, p x<VAR>c : R<GOAL>∀ᵐ (x : α) ∂c • μ, p x
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : α → Prop<VAR>ν : MeasureTheory.Measure α<GOAL>(∀ᵐ (x : α) ∂μ + ν, p x) ↔ (∀ᵐ (x : α) ∂μ, p x) ∧ ∀ᵐ (x : α) ∂ν, p x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>f : α → β<VAR>g g' : β → δ<VAR>hf : AEMeasurable f μ<VAR>h : g =ᵐ[ν] g'<VAR>h2 : MeasureTheory.Measure.map f μ ≪ ν<GOAL>g ∘ f =ᵐ[μ] g' ∘ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>f : α → β<VAR>g g' : β → δ<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν<VAR>h : g =ᵐ[ν] g'<GOAL>g ∘ f =ᵐ[μ] g' ∘ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>g g' : β → δ<VAR>hf : AEMeasurable f μ<VAR>h : g =ᵐ[MeasureTheory.Measure.map f μ] g'<GOAL>g ∘ f =ᵐ[μ] g' ∘ f
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>Group β<VAR>f g : α → β<GOAL>f / g =ᵐ[μ] 1 ↔ f =ᵐ[μ] g
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>AddGroup β<VAR>f g : α → β<GOAL>f - g =ᵐ[μ] 0 ↔ f =ᵐ[μ] g
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>Group β<VAR>LE β<VAR>CovariantClass β β (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>f g : α → β<GOAL>1 ≤ᵐ[μ] g / f ↔ f ≤ᵐ[μ] g
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>AddGroup β<VAR>LE β<VAR>CovariantClass β β (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>f g : α → β<GOAL>0 ≤ᵐ[μ] g - f ↔ f ≤ᵐ[μ] g
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>MeasureTheory.ae μ ⊓ 𝓟 s ≤ MeasureTheory.ae (μ.restrict s)
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.ae (μ.restrict s) = MeasureTheory.ae μ ⊓ 𝓟 s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>MeasureTheory.ae (μ.restrict s) = ⊥ ↔ μ s = 0
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>(MeasureTheory.ae (μ.restrict s)).NeBot ↔ μ s ≠ 0
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>s ∈ MeasureTheory.ae (μ.restrict s)
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : α → Prop<VAR>hst : s =ᵐ[μ] t<VAR>p : α → Prop<GOAL>(∀ᵐ (x : α) ∂μ.restrict s, p x) → ∀ᵐ (x : α) ∂μ.restrict t, p x
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : α → Prop<VAR>hst : s =ᵐ[μ] t<VAR>p : α → Prop<GOAL>(∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ.restrict t, p x
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℕ → α → Prop<VAR>hp : ∑' (i : ℕ), μ {x | p i x} ≠ ⊤<GOAL>μ {x | ∃ᶠ (n : ℕ) in Filter.atTop, p n x} = 0
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : ℕ → Set α<VAR>hs : ∑' (i : ℕ), μ (s i) ≠ ⊤<GOAL>∀ᵐ (x : α) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, x ∉ s n
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>MeasurableSpace β<VAR>b : β<VAR>f : α → β<VAR>s : Set α<VAR>f_mble : MeasureTheory.NullMeasurable f (μ.restrict s)<VAR>hs : f =ᵐ[μ.restrict sᶜ] fun x => b<VAR>t : Set β<VAR>t_mble : MeasurableSet t<VAR>ht : b ∉ t<GOAL>μ (f ⁻¹' t) = (μ.restrict s) (f ⁻¹' t)
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>t : Set ↑s<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>ht : MeasurableSet t<GOAL>MeasureTheory.NullMeasurableSet (Subtype.val '' t) μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>t : Set ↑s<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>ht : MeasureTheory.NullMeasurableSet t (MeasureTheory.Measure.comap Subtype.val μ)<GOAL>MeasureTheory.NullMeasurableSet (Subtype.val '' t) μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>t : Set ↑s<GOAL>μ (Subtype.val '' t) ≤ (MeasureTheory.Measure.comap Subtype.val μ) t
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>t : Set ↑s<VAR>ht : (MeasureTheory.Measure.comap Subtype.val μ) t = 0<GOAL>μ (Subtype.val '' t) = 0
<VAR>δ : Type u_4<VAR>u : Set δ<VAR>MeasureTheory.MeasureSpace δ<GOAL>MeasureTheory.volume = MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume
<VAR>δ : Type u_4<VAR>u : Set δ<VAR>MeasureTheory.MeasureSpace δ<VAR>hu : MeasureTheory.NullMeasurableSet u MeasureTheory.volume<GOAL>MeasureTheory.volume Set.univ = MeasureTheory.volume u
<VAR>δ : Type u_4<VAR>u : Set δ<VAR>MeasureTheory.MeasureSpace δ<VAR>hu : MeasureTheory.NullMeasurableSet u MeasureTheory.volume<VAR>t : Set ↑u<GOAL>MeasureTheory.volume (Subtype.val '' t) ≤ MeasureTheory.volume t
<VAR>δ : Type u_4<VAR>u : Set δ<VAR>MeasureTheory.MeasureSpace δ<VAR>hu : MeasureTheory.NullMeasurableSet u MeasureTheory.volume<VAR>t : Set ↑u<VAR>ht : MeasureTheory.volume t = 0<GOAL>MeasureTheory.volume (Subtype.val '' t) = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ : MeasureTheory.Measure β<GOAL>MeasureTheory.Measure.map f (MeasureTheory.Measure.comap f μ) = μ.restrict (Set.range f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ : MeasureTheory.Measure β<VAR>s : Set α<GOAL>(MeasureTheory.Measure.comap f μ) s = μ (f '' s)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.Measure.comap f (MeasureTheory.Measure.map f μ) = μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>p : β → Prop<VAR>μ : MeasureTheory.Measure α<GOAL>(∀ᵐ (x : β) ∂MeasureTheory.Measure.map f μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p (f x)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ : MeasureTheory.Measure α<VAR>s : Set β<GOAL>(MeasureTheory.Measure.map f μ).restrict s = MeasureTheory.Measure.map f (μ.restrict (f ⁻¹' s))
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ : MeasureTheory.Measure β<VAR>s : Set β<GOAL>(MeasureTheory.Measure.comap f μ) (f ⁻¹' s) = μ (s ∩ Set.range f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ : MeasureTheory.Measure β<VAR>s : Set β<GOAL>MeasureTheory.Measure.comap f (μ.restrict s) = (MeasureTheory.Measure.comap f μ).restrict (f ⁻¹' s)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ : MeasureTheory.Measure β<VAR>s : Set α<GOAL>(MeasureTheory.Measure.comap f μ).restrict s = MeasureTheory.Measure.comap f (μ.restrict (f '' s))
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>e : α ≃ᵐ β<VAR>μ : MeasureTheory.Measure α<VAR>s : Set β<GOAL>(MeasureTheory.Measure.map (⇑e) μ).restrict s = MeasureTheory.Measure.map (⇑e) (μ.restrict (⇑e ⁻¹' s))
<VAR>α : Type u_2<VAR>_m0 : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>μ : MeasureTheory.Measure α<VAR>t : Set ↑s<GOAL>(MeasureTheory.Measure.comap Subtype.val μ) t = μ (Subtype.val '' t)
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.Measure.map Subtype.val (MeasureTheory.Measure.comap Subtype.val μ) = μ.restrict s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>p : α → Prop<GOAL>(∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : ↑s) ∂MeasureTheory.Measure.comap Subtype.val μ, p ↑x
<VAR>α : Type u_2<VAR>MeasureTheory.MeasureSpace α<VAR>s : Set α<GOAL>MeasureTheory.volume = MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume
<VAR>α : Type u_2<VAR>MeasureTheory.MeasureSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.Measure.map Subtype.val MeasureTheory.volume = MeasureTheory.volume.restrict s
<VAR>α : Type u_2<VAR>MeasureTheory.MeasureSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set ↑s<GOAL>MeasureTheory.volume (Subtype.val '' t) = MeasureTheory.volume t
<VAR>α : Type u_2<VAR>MeasureTheory.MeasureSpace α<VAR>s t : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume<VAR>ht : MeasurableSet t<GOAL>MeasureTheory.volume (Subtype.val ⁻¹' t) = MeasureTheory.volume (t ∩ s)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f g : α → β<VAR>DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<GOAL>s.piecewise f g =ᵐ[μ.restrict s] f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f g : α → β<VAR>DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<GOAL>s.piecewise f g =ᵐ[μ.restrict sᶜ] g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>f g : α → β<VAR>DecidablePred fun x => x ∈ s<VAR>DecidablePred fun x => x ∈ t<VAR>hst : s =ᵐ[μ] t<GOAL>s.piecewise f g =ᵐ[μ] t.piecewise f g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → β<VAR>Zero β<VAR>t : Set β<VAR>ht : 0 ∈ t<VAR>hs : MeasurableSet s<GOAL>t ∈ Filter.map (s.indicator f) (MeasureTheory.ae μ) ↔ t ∈ Filter.map f (MeasureTheory.ae (μ.restrict s))
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → β<VAR>Zero β<VAR>t : Set β<VAR>ht : 0 ∉ t<GOAL>t ∈ Filter.map (s.indicator f) (MeasureTheory.ae μ) ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → β<VAR>Zero β<VAR>hs : MeasurableSet s<GOAL>Filter.map f (MeasureTheory.ae (μ.restrict s)) ≤ Filter.map (s.indicator f) (MeasureTheory.ae μ)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → β<VAR>Zero β<VAR>hs : MeasurableSet s<GOAL>s.indicator f =ᵐ[μ.restrict s] f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → β<VAR>Zero β<VAR>hs : MeasurableSet s<GOAL>s.indicator f =ᵐ[μ.restrict sᶜ] 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → β<VAR>Zero β<VAR>hs : MeasurableSet s<VAR>hf : f =ᵐ[μ.restrict sᶜ] 0<GOAL>s.indicator f =ᵐ[μ] f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → β<VAR>Zero β<VAR>hs : MeasurableSet s<VAR>hf : f =ᵐ[μ.restrict s] 0<GOAL>s.indicator f =ᵐ[μ] 0