ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<VAR>LinearOrder α<VAR>a b : α<GOAL>Ι a b =ᵐ[μ] Set.uIcc a b
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>γ : Type u_5<VAR>f g : α → γ<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>hs_zero : μ s = 0<GOAL>(fun x => if x ∈ s then f x else g x) =ᵐ[μ] g
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>γ : Type u_5<VAR>f g : α → γ<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>hs_zero : μ sᶜ = 0<GOAL>(fun x => if x ∈ s then f x else g x) =ᵐ[μ] f
<VAR>α : Type u_1<VAR>_m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : Filter α<GOAL>μ.FiniteAtFilter f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : Filter α<VAR>hμ : μ.FiniteAtFilter f<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hf : f.HasBasis p s<GOAL>∃ i, p i ∧ μ (s i) < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ.FiniteAtFilter ⊥
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>C : Set (Set α)<VAR>self : μ.FiniteSpanningSetsIn C<VAR>i : ℕ<GOAL>μ (self.set i) < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>C : Set (Set α)<VAR>self : μ.FiniteSpanningSetsIn C<GOAL>⋃ i, self.set i = Set.univ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>C : Set (Set α)<VAR>self : μ.FiniteSpanningSetsIn C<VAR>i : ℕ<GOAL>self.set i ∈ C
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>self : MeasureTheory.SFinite μ<GOAL>∃ m, (∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (m n)) ∧ μ = MeasureTheory.Measure.sum m
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.SFinite μ<GOAL>MeasureTheory.Measure.sum (MeasureTheory.sFiniteSeq μ) = μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>n : ℕ<GOAL>MeasureTheory.sFiniteSeq 0 n = 0
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>Countable ι<VAR>m : ι → MeasureTheory.Measure α<VAR>∀ (n : ι), MeasureTheory.IsFiniteMeasure (m n)<GOAL>MeasureTheory.SFinite (MeasureTheory.Measure.sum m)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<GOAL>∃ ν, MeasureTheory.IsFiniteMeasure ν ∧ μ ≪ ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>self : MeasureTheory.SigmaFinite μ<GOAL>Nonempty (μ.FiniteSpanningSetsIn Set.univ)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.SigmaFinite μ ↔ Nonempty (μ.FiniteSpanningSetsIn Set.univ)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.SigmaFinite μ<GOAL>Nonempty (μ.FiniteSpanningSetsIn Set.univ)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>Monotone (MeasureTheory.spanningSets μ)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>i : ℕ<GOAL>MeasurableSet (MeasureTheory.spanningSets μ i)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>i : ℕ<GOAL>μ (MeasureTheory.spanningSets μ i) < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>⋃ i, MeasureTheory.spanningSets μ i = Set.univ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>IsCountablySpanning (Set.range (MeasureTheory.spanningSets μ))
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>Measurable (MeasureTheory.spanningSetsIndex μ)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>n : ℕ<GOAL>MeasureTheory.spanningSetsIndex μ ⁻¹' {n} = disjointed (MeasureTheory.spanningSets μ) n
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>x : α<VAR>n : ℕ<GOAL>MeasureTheory.spanningSetsIndex μ x = n ↔ x ∈ disjointed (MeasureTheory.spanningSets μ) n
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>x : α<GOAL>x ∈ disjointed (MeasureTheory.spanningSets μ) (MeasureTheory.spanningSetsIndex μ x)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>x : α<GOAL>x ∈ MeasureTheory.spanningSets μ (MeasureTheory.spanningSetsIndex μ x)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>x : α<VAR>n : ℕ<VAR>hn : MeasureTheory.spanningSetsIndex μ x ≤ n<GOAL>x ∈ MeasureTheory.spanningSets μ n
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>x : α<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, x ∈ MeasureTheory.spanningSets μ n
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite ν<GOAL>(MeasureTheory.Measure.sum fun n => μ.restrict (disjointed (MeasureTheory.spanningSets ν) n)) = μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>s : Set α<GOAL>(∀ (n : ℕ), μ (s ∩ MeasureTheory.spanningSets μ n) = 0) ↔ μ s = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>s : Set α<GOAL>(∃ n, 0 < μ (s ∩ MeasureTheory.spanningSets μ n)) ↔ 0 < μ s
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ε : ℝ≥0∞<VAR>ε_pos : 0 < ε<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ<VAR>As_disj : Pairwise (MeasureTheory.AEDisjoint μ on As)<VAR>Union_As_finite : μ (⋃ i, As i) ≠ ⊤<GOAL>{i | ε ≤ μ (As i)}.Finite
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ε : ℝ≥0∞<VAR>ε_pos : 0 < ε<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), MeasurableSet (As i)<VAR>As_disj : Pairwise (Disjoint on As)<VAR>Union_As_finite : μ (⋃ i, As i) ≠ ⊤<GOAL>{i | ε ≤ μ (As i)}.Finite
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSingletonClass α<VAR>s : Set α<VAR>hs : s.Infinite<VAR>h' : ∃ ε, ε ≠ 0 ∧ ∀ x ∈ s, ε ≤ μ {x}<GOAL>μ s = ⊤
<VAR>α : Type u_1<VAR>ι : Type u_5<GOAL>∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) {As : ι → Set α}, (∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) → Pairwise (MeasureTheory.AEDisjoint μ on As) → μ (⋃ i, As i) ≠ ⊤ → {i | 0 < μ (As i)}.Countable
<VAR>α : Type u_1<VAR>ι : Type u_5<GOAL>∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) {As : ι → Set α}, (∀ (i : ι), MeasurableSet (As i)) → Pairwise (Disjoint on As) → μ (⋃ i, As i) ≠ ⊤ → {i | 0 < μ (As i)}.Countable
<VAR>α : Type u_1<VAR>ι : Type u_5<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ] {As : ι → Set α}, (∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) → Pairwise (MeasureTheory.AEDisjoint μ on As) → {i | 0 < μ (As i)}.Countable
<VAR>α : Type u_1<VAR>ι : Type u_5<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ] {As : ι → Set α}, (∀ (i : ι), MeasurableSet (As i)) → Pairwise (Disjoint on As) → {i | 0 < μ (As i)}.Countable
<VAR>α : Type u_5<VAR>β : Type u_6<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ] [inst : MeasurableSpace β] [inst_1 : MeasurableSingletonClass β] {g : α → β}, MeasureTheory.NullMeasurable g μ → {t | 0 < μ {a | g a = t}}.Countable
<VAR>α : Type u_5<VAR>β : Type u_6<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ] [inst : MeasurableSpace β] [inst_1 : MeasurableSingletonClass β] {g : α → β}, Measurable g → {t | 0 < μ {a | g a = t}}.Countable
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>m : ℕ → MeasureTheory.Measure α<VAR>hv : ∀ (n : ℕ), (m n) t ≠ ⊤<VAR>hμ : μ = MeasureTheory.Measure.sum m<GOAL>μ (MeasureTheory.toMeasurable μ t ∩ s) = μ (t ∩ s)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>v : ℕ → Set α<VAR>hv : t ⊆ ⋃ n, v n<VAR>h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ⊤<GOAL>μ (MeasureTheory.toMeasurable μ t ∩ s) = μ (t ∩ s)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>v : ℕ → Set α<VAR>hv : s ⊆ ⋃ n, v n<VAR>h'v : ∀ (n : ℕ), μ (s ∩ v n) ≠ ⊤<GOAL>μ.restrict (MeasureTheory.toMeasurable μ s) = μ.restrict s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<GOAL>μ (MeasureTheory.toMeasurable μ t ∩ s) = μ (t ∩ s)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>s : Set α<GOAL>μ.restrict (MeasureTheory.toMeasurable μ s) = μ.restrict s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasureTheory.SigmaFinite μ<VAR>hs : MeasurableSet s<GOAL>⨆ i, (μ.restrict (MeasureTheory.spanningSets μ i)) s = μ s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>s : Set α<GOAL>⨆ i, (μ.restrict (MeasureTheory.spanningSets μ i)) s = μ s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasureTheory.SigmaFinite μ<VAR>r : ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>h's : r < μ s<GOAL>∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>C : Set (Set α)<VAR>h : μ.FiniteSpanningSetsIn C<GOAL>MeasureTheory.SigmaFinite μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>C : Set (Set α)<VAR>hA : m0 = MeasurableSpace.generateFrom C<VAR>hC : IsPiSystem C<VAR>h : μ.FiniteSpanningSetsIn C<VAR>h_eq : ∀ s ∈ C, μ s = ν s<GOAL>μ = ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>C : Set (Set α)<VAR>h : μ.FiniteSpanningSetsIn C<GOAL>IsCountablySpanning C
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>S : Set (Set α)<VAR>hc : S.Countable<VAR>hμ : ∀ s ∈ S, μ s < ⊤<VAR>hU : ⋃₀ S = Set.univ<GOAL>MeasureTheory.SigmaFinite μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>μ : MeasureTheory.Measure α<VAR>hs : MeasureTheory.SigmaFinite μ<VAR>h : ν ≤ μ<GOAL>MeasureTheory.SigmaFinite ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν₁ ν₂ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>μ + ν₁ = μ + ν₂ ↔ ν₁ = ν₂
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν₁ ν₂ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>ν₁ + μ = ν₂ + μ ↔ ν₁ = ν₂
<VAR>α : Type u_1<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.SigmaFinite μ ↔ MeasureTheory.IsFiniteMeasure μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>h : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map f μ)<GOAL>MeasureTheory.SigmaFinite μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>MeasureTheory.SigmaFinite μ<GOAL>MeasureTheory.SigmaFinite (MeasureTheory.Measure.map f μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α ≃ᵐ β<VAR>MeasureTheory.SigmaFinite μ<GOAL>MeasureTheory.SigmaFinite (MeasureTheory.Measure.map (⇑f) μ)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>P : α → Prop<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ν s < ⊤ → ∀ᵐ (x : α) ∂μ.restrict s, P x<GOAL>∀ᵐ (x : α) ∂μ, P x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>P : α → Prop<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ᵐ (x : α) ∂μ.restrict s, P x<GOAL>∀ᵐ (x : α) ∂μ, P x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>self : MeasureTheory.IsLocallyFiniteMeasure μ<VAR>x : α<GOAL>μ.FiniteAtFilter (𝓝 x)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>x : α<GOAL>μ.FiniteAtFilter (𝓝 x)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>MeasureTheory.IsFiniteMeasure (c • μ)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>x : α<GOAL>∃ s, x ∈ s ∧ IsOpen s ∧ μ s < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>TopologicalSpace.IsTopologicalBasis {s | IsOpen s ∧ μ s < ⊤}
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>self : MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>K : Set α<GOAL>IsCompact K → μ K < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>K : Set α<VAR>hK : IsCompact K<GOAL>μ K < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>K : Set α<VAR>hK : IsCompact K<GOAL>μ K ≠ ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>PseudoMetricSpace α<VAR>ProperSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>s : Set α<VAR>hs : Bornology.IsBounded s<GOAL>μ s < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>PseudoMetricSpace α<VAR>ProperSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>x : α<VAR>r : ℝ<GOAL>μ (Metric.closedBall x r) < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>PseudoMetricSpace α<VAR>ProperSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>x : α<VAR>r : ℝ<GOAL>μ (Metric.ball x r) < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>MeasureTheory.IsFiniteMeasureOnCompacts (c • μ)
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>U : ι → Set α<VAR>hU : ⋃ i, U i = Set.univ<VAR>hμ : μ ≠ 0<GOAL>∃ i, 0 < μ (U i)
<VAR>α : Type u_1<VAR>δ : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>PseudoMetricSpace δ<VAR>f : α → δ<VAR>x : δ<VAR>hμ : μ ≠ 0<GOAL>∃ n, 0 < μ (f ⁻¹' Metric.ball x ↑n)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>PseudoMetricSpace α<VAR>x : α<VAR>hμ : μ ≠ 0<GOAL>∃ n, 0 < μ (Metric.ball x ↑n)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>TopologicalSpace β<VAR>T1Space β<VAR>SecondCountableTopology β<VAR>Nonempty β<VAR>f : α → β<VAR>h : ∀ (b : β), ∃ᵐ (x : α) ∂μ, f x ≠ b<GOAL>∃ a b, a ≠ b ∧ (∀ s ∈ 𝓝 a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ 𝓝 b, 0 < μ (f ⁻¹' t)
<VAR>α : Type u_5<VAR>m₀ : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>C : Set (Set α)<VAR>hμν : ∀ s ∈ C, μ s = ν s<VAR>m : MeasurableSpace α<VAR>h : m ≤ m₀<VAR>hA : m = MeasurableSpace.generateFrom C<VAR>hC : IsPiSystem C<VAR>h_univ : μ Set.univ = ν Set.univ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ s = ν s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>C : Set (Set α)<VAR>hA : m0 = MeasurableSpace.generateFrom C<VAR>hC : IsPiSystem C<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hμν : ∀ s ∈ C, μ s = ν s<VAR>h_univ : μ Set.univ = ν Set.univ<GOAL>μ = ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>S : μ.FiniteSpanningSetsIn {s | MeasurableSet s}<GOAL>S.disjointed.set = disjointed S.set
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<GOAL>∃ S T, S.set = T.set ∧ Pairwise (Disjoint on S.set)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : Filter α<VAR>h : f ≤ g<GOAL>μ.FiniteAtFilter g → μ.FiniteAtFilter f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : Filter α<VAR>h : μ.FiniteAtFilter f<GOAL>μ.FiniteAtFilter (f ⊓ g)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : Filter α<VAR>h : μ.FiniteAtFilter g<GOAL>μ.FiniteAtFilter (f ⊓ g)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : Filter α<GOAL>μ.FiniteAtFilter (f ⊓ MeasureTheory.ae μ) ↔ μ.FiniteAtFilter f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : Filter α<VAR>h : f ⊓ MeasureTheory.ae μ ≤ g<VAR>hg : μ.FiniteAtFilter g<GOAL>μ.FiniteAtFilter f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f : Filter α<VAR>h : μ ≤ ν<GOAL>ν.FiniteAtFilter f → μ.FiniteAtFilter f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f g : Filter α<VAR>hf : f ≤ g<VAR>hμ : μ ≤ ν<GOAL>ν.FiniteAtFilter g → μ.FiniteAtFilter f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : Filter α<VAR>h : μ.FiniteAtFilter f<GOAL>∀ᶠ (s : Set α) in f.smallSets, μ s < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : Filter α<GOAL>μ.FiniteAtFilter f → μ.FiniteAtFilter g → μ.FiniteAtFilter (f ⊔ g)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>_m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>x : α<VAR>s : Set α<GOAL>μ.FiniteAtFilter (𝓝[s] x)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>μ.FiniteAtFilter (𝓟 s) ↔ μ s < ⊤
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>_m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>H : MeasureTheory.IsLocallyFiniteMeasure μ<VAR>h : ν ≤ μ<GOAL>MeasureTheory.IsLocallyFiniteMeasure ν
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : IsCompact s<VAR>hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)<GOAL>∃ U ⊇ s, IsOpen U ∧ μ U < ⊤
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>h : IsCompact s<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>∃ U ⊇ s, IsOpen U ∧ μ U < ⊤
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : IsCompact s<VAR>hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝[s] x)<GOAL>μ s < ⊤
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : IsCompact s<GOAL>(∀ a ∈ s, ∃ t ∈ 𝓝[s] a, μ t = 0) → μ s = 0
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompactSpace α<GOAL>MeasureTheory.IsFiniteMeasure μ ↔ MeasureTheory.IsFiniteMeasureOnCompacts μ
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>μ.finiteSpanningSetsInOpen' = let_fun H := ⋯; H.some
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>CompactIccSpace α<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>a b : α<GOAL>μ (Set.Icc a b) < ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>CompactIccSpace α<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>a b : α<GOAL>μ (Set.Ico a b) < ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>CompactIccSpace α<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>a b : α<GOAL>μ (Set.Ioc a b) < ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>CompactIccSpace α<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>a b : α<GOAL>μ (Set.Ioo a b) < ⊤
<VAR>M : Type u<VAR>NormedRing M<VAR>StarRing M<VAR>CstarRing M<VAR>Module ℂ M<VAR>NormedAlgebra ℂ M<VAR>StarModule ℂ M<VAR>self : WStarAlgebra M<GOAL>∃ X x x_1, ∃ (_ : CompleteSpace X), Nonempty (NormedSpace.Dual ℂ X ≃ₗᵢ⋆[ℂ] M)
<VAR>H : Type u<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℂ H<VAR>CompleteSpace H<VAR>self : VonNeumannAlgebra H<GOAL>self.carrier.centralizer.centralizer = self.carrier
<VAR>H : Type u<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℂ H<VAR>CompleteSpace H<VAR>S : VonNeumannAlgebra H<VAR>x : H →L[ℂ] H<GOAL>x ∈ S.toStarSubalgebra ↔ x ∈ ↑S
<VAR>H : Type u<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℂ H<VAR>CompleteSpace H<VAR>S : VonNeumannAlgebra H<GOAL>↑S.toStarSubalgebra = ↑S
<VAR>H : Type u<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℂ H<VAR>CompleteSpace H<VAR>S : StarSubalgebra ℂ (H →L[ℂ] H)<VAR>h : S.carrier.centralizer.centralizer = S.carrier<GOAL>↑{ toStarSubalgebra := S, centralizer_centralizer' := h } = ↑S
<VAR>H : Type u<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℂ H<VAR>CompleteSpace H<VAR>S T : VonNeumannAlgebra H<VAR>h : ∀ (x : H →L[ℂ] H), x ∈ S ↔ x ∈ T<GOAL>S = T
<VAR>H : Type u<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℂ H<VAR>CompleteSpace H<VAR>S : VonNeumannAlgebra H<GOAL>(↑S).centralizer.centralizer = ↑S
<VAR>H : Type u<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℂ H<VAR>CompleteSpace H<VAR>S : VonNeumannAlgebra H<GOAL>↑S.commutant = (↑S).centralizer
<VAR>H : Type u<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℂ H<VAR>CompleteSpace H<VAR>S : VonNeumannAlgebra H<VAR>z : H →L[ℂ] H<GOAL>z ∈ S.commutant ↔ ∀ g ∈ S, g * z = z * g
<VAR>H : Type u<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℂ H<VAR>CompleteSpace H<VAR>S : VonNeumannAlgebra H<GOAL>S.commutant.commutant = S
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>ν : MeasureTheory.FiniteMeasure Ω<GOAL>↑ν = ↑ν
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<GOAL>Function.Injective MeasureTheory.FiniteMeasure.toMeasure
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<GOAL>⇑μ = fun s => (↑μ s).toNNReal
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>hμ : MeasureTheory.IsFiniteMeasure μ<GOAL>⇑⟨μ, hμ⟩ = fun s => (μ s).toNNReal
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>hμ : MeasureTheory.IsFiniteMeasure μ<VAR>s : Set Ω<GOAL>⟨μ, hμ⟩ s = (μ s).toNNReal
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>ν : MeasureTheory.FiniteMeasure Ω<VAR>s : Set Ω<GOAL>↑(ν s) = ↑ν s
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>s₁ s₂ : Set Ω<VAR>h : s₁ ⊆ s₂<GOAL>μ s₁ ≤ μ s₂
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>s : Set Ω<GOAL>μ s ≤ μ.mass
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<GOAL>↑μ.mass = ↑μ Set.univ
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<GOAL>⇑0 = 0
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<GOAL>MeasureTheory.FiniteMeasure.mass 0 = 0
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<GOAL>μ.mass = 0 ↔ μ = 0
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<GOAL>μ.mass ≠ 0 ↔ μ ≠ 0
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ ν : MeasureTheory.FiniteMeasure Ω<VAR>h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s<GOAL>μ = ν
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ ν : MeasureTheory.FiniteMeasure Ω<VAR>h : ∀ (s : Set Ω), MeasurableSet s → μ s = ν s<GOAL>μ = ν
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<GOAL>↑0 = 0