ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>μ'.IsAddHaarMeasure<GOAL>0 < μ'.addHaarScalarFactor μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>μ'.IsHaarMeasure<GOAL>0 < μ'.haarScalarFactor μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsAddLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<GOAL>μ' (f ⁻¹' {1}) = μ'.addHaarScalarFactor μ • μ (f ⁻¹' {1})
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsMulLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<GOAL>μ' (f ⁻¹' {1}) = μ'.haarScalarFactor μ • μ (f ⁻¹' {1})
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsMulLeftInvariant<VAR>μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<GOAL>μ'.haarScalarFactor μ • μ s ≤ μ' s
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsAddLeftInvariant<VAR>μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<GOAL>μ'.addHaarScalarFactor μ • μ s ≤ μ' s
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsAddLeftInvariant<VAR>μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<GOAL>μ' s = μ'.addHaarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsMulLeftInvariant<VAR>μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<GOAL>μ' s = μ'.haarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsAddLeftInvariant<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<GOAL>μ' s = μ'.addHaarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsMulLeftInvariant<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<GOAL>μ' s = μ'.haarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsMulLeftInvariant<VAR>s : Set G<VAR>h's : IsCompact (closure s)<GOAL>μ' s = μ'.haarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsAddLeftInvariant<VAR>s : Set G<VAR>h's : IsCompact (closure s)<GOAL>μ' s = μ'.addHaarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>CompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>μ'.IsMulLeftInvariant<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<GOAL>μ' = μ'.haarScalarFactor μ • μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>CompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>μ'.IsAddLeftInvariant<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<GOAL>μ' = μ'.addHaarScalarFactor μ • μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>MeasureTheory.IsProbabilityMeasure μ'<VAR>μ.IsHaarMeasure<VAR>μ'.IsHaarMeasure<GOAL>μ' = μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>MeasureTheory.IsProbabilityMeasure μ'<VAR>μ.IsAddHaarMeasure<VAR>μ'.IsAddHaarMeasure<GOAL>μ' = μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>μ'.IsAddHaarMeasure<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : μ.IsEverywherePos s<GOAL>μ' s = μ'.addHaarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>μ'.IsHaarMeasure<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : μ.IsEverywherePos s<GOAL>μ' s = μ'.haarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>μ'.IsHaarMeasure<VAR>s : Set G<VAR>hs : IsOpen s<GOAL>μ' s = μ'.haarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>μ'.IsAddHaarMeasure<VAR>s : Set G<VAR>hs : IsOpen s<GOAL>μ' s = μ'.addHaarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsAddLeftInvariant<VAR>μ.InnerRegularCompactLTTop<VAR>μ'.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : μ s ≠ ⊤<VAR>h's : μ' s ≠ ⊤<GOAL>μ' s = μ'.addHaarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsMulLeftInvariant<VAR>μ.InnerRegularCompactLTTop<VAR>μ'.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : μ s ≠ ⊤<VAR>h's : μ' s ≠ ⊤<GOAL>μ' s = μ'.haarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsMulLeftInvariant<VAR>μ.InnerRegular<VAR>μ'.InnerRegular<GOAL>μ' = μ'.haarScalarFactor μ • μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsAddLeftInvariant<VAR>μ.InnerRegular<VAR>μ'.InnerRegular<GOAL>μ' = μ'.addHaarScalarFactor μ • μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsAddLeftInvariant<VAR>μ.Regular<VAR>μ'.Regular<GOAL>μ' = μ'.addHaarScalarFactor μ • μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsMulLeftInvariant<VAR>μ.Regular<VAR>μ'.Regular<GOAL>μ' = μ'.haarScalarFactor μ • μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>SecondCountableTopology G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsMulLeftInvariant<GOAL>μ' = μ'.haarScalarFactor μ • μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>SecondCountableTopology G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsAddLeftInvariant<GOAL>μ' = μ'.addHaarScalarFactor μ • μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>SecondCountableTopology G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ<VAR>μ.IsAddLeftInvariant<VAR>ν.IsAddHaarMeasure<GOAL>μ ≪ ν
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>SecondCountableTopology G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ<VAR>μ.IsMulLeftInvariant<VAR>ν.IsHaarMeasure<GOAL>μ ≪ ν
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>CompactSpace G<VAR>DivisibleBy G ℤ<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>MeasureTheory.MeasurePreserving (fun g => n • g) μ μ
<VAR>G : Type u_1<VAR>CommGroup G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>CompactSpace G<VAR>RootableBy G ℤ<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>MeasureTheory.MeasurePreserving (fun g => g ^ n) μ μ
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>CompactSpace G<VAR>DivisibleBy G ℤ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>X : Type u_2<VAR>MeasurableSpace X<VAR>μ' : MeasureTheory.Measure X<VAR>f : X → G<VAR>hf : MeasureTheory.MeasurePreserving f μ' μ<GOAL>MeasureTheory.MeasurePreserving (fun x => n • f x) μ' μ
<VAR>G : Type u_1<VAR>CommGroup G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>CompactSpace G<VAR>RootableBy G ℤ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>X : Type u_2<VAR>MeasurableSpace X<VAR>μ' : MeasureTheory.Measure X<VAR>f : X → G<VAR>hf : MeasureTheory.MeasurePreserving f μ' μ<GOAL>MeasureTheory.MeasurePreserving (fun x => f x ^ n) μ' μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>self : MeasureTheory.IsFiniteMeasure μ<GOAL>μ Set.univ < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>¬MeasureTheory.IsFiniteMeasure μ ↔ μ Set.univ = ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : Set α<GOAL>μ s < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : Set α<GOAL>μ s ≠ ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>ε : ℝ≥0∞<VAR>h : μ s ≤ μ t + ε<GOAL>μ tᶜ ≤ μ sᶜ + ε
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>ε : ℝ≥0∞<GOAL>μ sᶜ ≤ μ tᶜ + ε ↔ μ t ≤ μ s + ε
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>↑(MeasureTheory.measureUnivNNReal μ) = μ Set.univ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<GOAL>MeasureTheory.measureUnivNNReal 0 = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h : ν ≤ μ<GOAL>MeasureTheory.IsFiniteMeasure ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → β<GOAL>MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.map f μ)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>MeasureTheory.measureUnivNNReal μ = 0 ↔ μ = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<GOAL>0 < MeasureTheory.measureUnivNNReal μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν₁ ν₂ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>A2 : μ + ν₁ ≤ μ + ν₂<GOAL>ν₁ ≤ ν₂
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hμ : MeasureTheory.IsFiniteMeasure μ<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<GOAL>Summable fun x => (μ (f x)).toReal
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>s =ᵐ[μ] Set.univ ↔ μ s = μ Set.univ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>p : α → Prop<VAR>hp : MeasureTheory.NullMeasurableSet {a | p a} μ<GOAL>(∀ᵐ (a : α) ∂μ, p a) ↔ μ {a | p a} = μ Set.univ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>(∀ᵐ (a : α) ∂μ, a ∈ s) ↔ μ s = μ Set.univ
<VAR>X : Type u_5<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>Es : ℕ → Set X<VAR>Es_mble : ∀ (i : ℕ), MeasurableSet (Es i)<VAR>Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)<GOAL>Filter.Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hs' : μ s ≠ ⊤<VAR>ht' : μ t ≠ ⊤<GOAL>|(μ s).toReal - (μ t).toReal| ≤ (μ (symmDiff s t)).toReal
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>|(μ s).toReal - (μ t).toReal| ≤ (μ (symmDiff s t)).toReal
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>self : MeasureTheory.IsProbabilityMeasure μ<GOAL>μ Set.univ = 1
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.IsProbabilityMeasure μ ↔ μ Set.univ = 1
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>μ ≠ 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>(MeasureTheory.ae μ).NeBot
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>h : MeasurableSet s<GOAL>μ s + μ sᶜ = 1
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>μ s ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>f : α → β<VAR>hf : AEMeasurable f μ<GOAL>MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map f μ)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>1 ≤ μ s ↔ μ s = 1
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>h : MeasureTheory.NullMeasurableSet s μ<GOAL>μ sᶜ = 1 - μ s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hs : MeasurableSet s<GOAL>μ sᶜ = 1 - μ s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>p : ℝ≥0∞<VAR>hμs : p < μ s<VAR>s_mble : MeasurableSet s<GOAL>μ sᶜ < 1 - p
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>p : ℝ≥0∞<VAR>hμs : p ≤ μ s<VAR>s_mble : MeasurableSet s<GOAL>μ sᶜ ≤ 1 - p
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>μ sᶜ = 0 ↔ μ s = 1
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hs : MeasurableSet s<GOAL>μ sᶜ = 0 ↔ μ s = 1
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>μ sᶜ = 1 ↔ μ s = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hs : MeasurableSet s<GOAL>μ sᶜ = 1 ↔ μ s = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>s ∈ MeasureTheory.ae μ ↔ μ s = 1
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hs : MeasurableSet s<GOAL>s ∈ MeasureTheory.ae μ ↔ μ s = 1
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>p : α → Prop<VAR>hp : Measurable p<GOAL>(∀ᵐ (a : α) ∂μ, p a) ↔ μ {a | p a} = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>f : β → α<VAR>hf : Function.Injective f<VAR>hf' : ∀ᵐ (a : α) ∂μ, a ∈ Set.range f<VAR>hf'' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (f '' s)<GOAL>MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.comap f μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>f : β → α<VAR>hf : MeasurableEmbedding f<VAR>hf' : ∀ᵐ (a : α) ∂μ, a ∈ Set.range f<GOAL>MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.comap f μ)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>self : MeasureTheory.NoAtoms μ<VAR>x : α<GOAL>μ {x} = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>s : Set α<VAR>hs : s.Subsingleton<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>a : α<GOAL>μ.restrict {a} = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>s : Set α<VAR>h : s.Countable<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>s : Set α<VAR>h : s.Countable<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<GOAL>∀ᵐ (x : α) ∂μ, x ∉ s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>s : Set α<VAR>h : s.Countable<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<GOAL>μ.restrict sᶜ = μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>a : α<GOAL>μ.restrict {a}ᶜ = μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>s : Set α<VAR>h : s.Finite<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>s : Finset α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<GOAL>μ ↑s = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>a : α<VAR>s : Set α<GOAL>insert a s =ᵐ[μ] s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>PartialOrder α<VAR>a : α<GOAL>Set.Iio a =ᵐ[μ] Set.Iic a
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>PartialOrder α<VAR>a : α<GOAL>Set.Ioi a =ᵐ[μ] Set.Ici a
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>PartialOrder α<VAR>a b : α<GOAL>Set.Ioo a b =ᵐ[μ] Set.Ioc a b
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>PartialOrder α<VAR>a b : α<GOAL>Set.Ioc a b =ᵐ[μ] Set.Icc a b
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>PartialOrder α<VAR>a b : α<GOAL>Set.Ioo a b =ᵐ[μ] Set.Ico a b
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>PartialOrder α<VAR>a b : α<GOAL>Set.Ioo a b =ᵐ[μ] Set.Icc a b
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>PartialOrder α<VAR>a b : α<GOAL>Set.Ico a b =ᵐ[μ] Set.Icc a b
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>PartialOrder α<VAR>a b : α<GOAL>Set.Ico a b =ᵐ[μ] Set.Ioc a b
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>PartialOrder α<VAR>a : α<GOAL>μ.restrict (Set.Iio a) = μ.restrict (Set.Iic a)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>PartialOrder α<VAR>a : α<GOAL>μ.restrict (Set.Ioi a) = μ.restrict (Set.Ici a)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>PartialOrder α<VAR>a b : α<GOAL>μ.restrict (Set.Ioo a b) = μ.restrict (Set.Ioc a b)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>PartialOrder α<VAR>a b : α<GOAL>μ.restrict (Set.Ioc a b) = μ.restrict (Set.Icc a b)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>PartialOrder α<VAR>a b : α<GOAL>μ.restrict (Set.Ioo a b) = μ.restrict (Set.Ico a b)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>PartialOrder α<VAR>a b : α<GOAL>μ.restrict (Set.Ioo a b) = μ.restrict (Set.Icc a b)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>PartialOrder α<VAR>a b : α<GOAL>μ.restrict (Set.Ico a b) = μ.restrict (Set.Icc a b)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>PartialOrder α<VAR>a b : α<GOAL>μ.restrict (Set.Ico a b) = μ.restrict (Set.Ioc a b)