ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.Regular<VAR>x : ℝ≥0∞<VAR>hx : x ≠ ⊤<GOAL>(x • μ).Regular
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>R1Space α<VAR>BorelSpace α<VAR>μ.Regular<VAR>A : Set α<VAR>h'A : μ A ≠ ⊤<GOAL>(μ.restrict A).Regular
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>Subsingleton α<GOAL>AEMeasurable f μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>Subsingleton β<GOAL>AEMeasurable f μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<GOAL>AEMeasurable f 0
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>m : MeasurableSpace α<VAR>hm : m ≤ m0<GOAL>AEMeasurable id μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>h : NeZero (MeasureTheory.Measure.map f μ)<GOAL>AEMeasurable f μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ ν : MeasureTheory.Measure α<VAR>hf : AEMeasurable f ν<VAR>hμν : μ ≪ ν<GOAL>AEMeasurable f μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ ν : MeasureTheory.Measure α<VAR>h : AEMeasurable f μ<VAR>h' : ν ≤ μ<GOAL>AEMeasurable f ν
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>ht : AEMeasurable f (μ.restrict t)<GOAL>AEMeasurable f (μ.restrict s)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ ν : MeasureTheory.Measure α<VAR>h : AEMeasurable f μ<VAR>h' : ν ≪ μ<GOAL>AEMeasurable f ν
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : AEMeasurable f (μ.restrict s)<GOAL>∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEMeasurable.mk f h x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : AEMeasurable f (μ.restrict s)<GOAL>f =ᶠ[MeasureTheory.ae μ ⊓ 𝓟 s] AEMeasurable.mk f h
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>Countable ι<VAR>μ : ι → MeasureTheory.Measure α<VAR>h : ∀ (i : ι), AEMeasurable f (μ i)<GOAL>AEMeasurable f (MeasureTheory.Measure.sum μ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>Countable ι<VAR>μ : ι → MeasureTheory.Measure α<GOAL>AEMeasurable f (MeasureTheory.Measure.sum μ) ↔ ∀ (i : ι), AEMeasurable f (μ i)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ ν : MeasureTheory.Measure α<GOAL>AEMeasurable f (μ + ν) ↔ AEMeasurable f μ ∧ AEMeasurable f ν
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ ν : MeasureTheory.Measure α<VAR>f : α → β<VAR>hμ : AEMeasurable f μ<VAR>hν : AEMeasurable f ν<GOAL>AEMeasurable f (μ + ν)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), AEMeasurable f (μ.restrict (s i))<GOAL>AEMeasurable f (μ.restrict (⋃ i, s i))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<GOAL>AEMeasurable f (μ.restrict (⋃ i, s i)) ↔ ∀ (i : ι), AEMeasurable f (μ.restrict (s i))
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<GOAL>AEMeasurable f (μ.restrict (s ∪ t)) ↔ AEMeasurable f (μ.restrict s) ∧ AEMeasurable f (μ.restrict t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>Monoid R<VAR>DistribMulAction R ℝ≥0∞<VAR>IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>h : AEMeasurable f μ<VAR>c : R<GOAL>AEMeasurable f (c • μ)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_5<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace δ<VAR>μ : MeasureTheory.Measure α<VAR>f : α → δ<VAR>g : δ → β<VAR>hg : AEMeasurable g (MeasureTheory.Measure.map f μ)<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (g ∘ f) μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_5<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace δ<VAR>μ : MeasureTheory.Measure α<VAR>f : α → δ<VAR>g : δ → β<VAR>hg : AEMeasurable g (MeasureTheory.Measure.map f μ)<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun x => g (f x)) μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_5<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace δ<VAR>μ : MeasureTheory.Measure α<VAR>f : α → δ<VAR>g : δ → β<VAR>hg : AEMeasurable g (MeasureTheory.Measure.map f μ)<VAR>hf : Measurable f<GOAL>AEMeasurable (g ∘ f) μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_5<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace δ<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure δ<VAR>f : α → δ<VAR>g : δ → β<VAR>hg : AEMeasurable g ν<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν<GOAL>AEMeasurable (g ∘ f) μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>μ : MeasureTheory.Measure α<VAR>g : β → γ<VAR>f : α → β<VAR>hg : AEMeasurable g (MeasureTheory.Measure.map f μ)<VAR>hf : AEMeasurable f μ<GOAL>MeasureTheory.Measure.map g (MeasureTheory.Measure.map f μ) = MeasureTheory.Measure.map (g ∘ f) μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>g : α → γ<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (fun x => (f x, g x)) μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>H : AEMeasurable f μ<VAR>t : Set β<VAR>ht : ∀ᵐ (x : α) ∂μ, f x ∈ t<VAR>h₀ : t.Nonempty<GOAL>∃ g, Measurable g ∧ Set.range g ⊆ t ∧ f =ᵐ[μ] g
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>Preorder β<VAR>Zero β<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>f_nn : ∀ᵐ (t : α) ∂μ, 0 ≤ f t<GOAL>∃ g, Measurable g ∧ 0 ≤ g ∧ f =ᵐ[μ] g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>h : AEMeasurable f μ<VAR>s : Set β<VAR>hfs : ∀ (x : α), f x ∈ s<GOAL>AEMeasurable (Set.codRestrict f s hfs) μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y<GOAL>AEMeasurable f μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>LinearOrder α<VAR>f : α → β<VAR>a b : α<GOAL>AEMeasurable f (μ.restrict (Ι a b)) ↔ AEMeasurable f (μ.restrict (Set.Ioc a b)) ∧ AEMeasurable f (μ.restrict (Set.Ioc b a))
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>μ.IsComplete<GOAL>AEMeasurable f μ ↔ Measurable f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>g : β → γ<VAR>hf : MeasurableEmbedding f<GOAL>AEMeasurable g (MeasureTheory.Measure.map f μ) ↔ AEMeasurable (g ∘ f) μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : MeasurableEmbedding g<VAR>μ : MeasureTheory.Measure α<GOAL>AEMeasurable (g ∘ f) μ ↔ AEMeasurable f μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<GOAL>AEMeasurable f (μ.restrict s) ↔ AEMeasurable (f ∘ Subtype.val) (MeasureTheory.Measure.comap Subtype.val μ)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>One β<GOAL>AEMeasurable (fun x => 1) μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>Zero β<GOAL>AEMeasurable (fun x => 0) μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<GOAL>AEMeasurable f (c • μ) ↔ AEMeasurable f μ
<VAR>β : Type u_3<VAR>MeasurableSpace β<VAR>α : Type u_7<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : α → β<VAR>hf : AEMeasurable f (μ.trim hm)<GOAL>AEMeasurable f μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : Measurable fun x => f ↑x<GOAL>AEMeasurable f (μ.restrict s)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>μ : MeasureTheory.Measure α<VAR>e : α ≃ᵐ β<VAR>f : β → γ<GOAL>AEMeasurable f (MeasureTheory.Measure.map (⇑e) μ) ↔ AEMeasurable (f ∘ ⇑e) μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>hfm : AEMeasurable f μ<VAR>s : Set α<GOAL>AEMeasurable f (μ.restrict s)
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>mβ : MeasurableSpace β<VAR>LinearOrder α<VAR>Filter.atTop.IsCountablyGenerated<VAR>x : α<VAR>g : α → β<VAR>g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Set.Ioc x t))<GOAL>AEMeasurable g (μ.restrict (Set.Ioi x))
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>Zero β<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>Zero β<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>Zero β<VAR>s : Set α<VAR>MeasurableSingletonClass β<VAR>b : β<VAR>NeZero b<GOAL>AEMeasurable (s.indicator fun x => b) μ ↔ MeasureTheory.NullMeasurableSet s μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>Zero β<VAR>hfm : AEMeasurable f μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>AEMeasurable (s.indicator f) μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>Zero β<VAR>hfm : AEMeasurable f μ<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>AEMeasurable (s.indicator f) μ
<VAR>α : Type u_2<VAR>δ : Type u_5<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace δ<VAR>μ : MeasureTheory.Measure α<VAR>f : α → δ<VAR>hf : AEMeasurable 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>δ : Type u_5<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace δ<VAR>μ ν : MeasureTheory.Measure α<VAR>f : α → δ<VAR>h : μ ≤ ν<VAR>hf : AEMeasurable f ν<GOAL>MeasureTheory.Measure.map f μ ≤ MeasureTheory.Measure.map f ν
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hc : MeasurableSpace.CountablyGenerated β<VAR>h : MeasureTheory.NullMeasurable f μ<GOAL>AEMeasurable f μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>t : Set β<VAR>MeasurableSpace.CountablyGenerated ↑t<VAR>h : MeasureTheory.NullMeasurable f μ<VAR>hft : ∀ᵐ (x : α) ∂μ, f x ∈ t<GOAL>AEMeasurable f μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>ι : Type u_7<VAR>m : ι → MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f (MeasureTheory.Measure.sum m)<GOAL>MeasureTheory.Measure.map f (MeasureTheory.Measure.sum m) = MeasureTheory.Measure.sum fun i => MeasureTheory.Measure.map f (m i)
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>ε : ℝ<GOAL>Metric.closedBall x ε =ᵐ[MeasureTheory.volume] Metric.ball x ε
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>I : Set (AddCircle T)<VAR>u x : AddCircle T<VAR>hu : IsOfFinAddOrder u<VAR>hI : I =ᵐ[MeasureTheory.volume] Metric.ball x (T / (2 * ↑(addOrderOf u)))<GOAL>MeasureTheory.IsAddFundamentalDomain (↥(AddSubgroup.zmultiples u)) I MeasureTheory.volume
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s I : Set (AddCircle T)<VAR>u x : AddCircle T<VAR>hu : IsOfFinAddOrder u<VAR>hs : u +ᵥ s =ᵐ[MeasureTheory.volume] s<VAR>hI : I =ᵐ[MeasureTheory.volume] Metric.ball x (T / (2 * ↑(addOrderOf u)))<GOAL>MeasureTheory.volume s = addOrderOf u • MeasureTheory.volume (s ∩ I)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSMul G α<VAR>c : G<GOAL>(MeasurableEquiv.smul c).toEquiv = MulAction.toPerm c
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableVAdd G α<VAR>c : G<GOAL>⇑(MeasurableEquiv.vadd c) = fun x => c +ᵥ x
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSMul G α<VAR>c : G<GOAL>⇑(MeasurableEquiv.smul c) = fun x => c • x
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableVAdd G α<VAR>c : G<GOAL>(MeasurableEquiv.vadd c).toEquiv = AddAction.toPerm c
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSMul G α<VAR>c : G<GOAL>MeasurableEmbedding fun x => c • x
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableVAdd G α<VAR>c : G<GOAL>MeasurableEmbedding fun x => c +ᵥ x
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSMul G α<VAR>c : G<GOAL>(MeasurableEquiv.smul c).symm = MeasurableEquiv.smul c⁻¹
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableVAdd G α<VAR>c : G<GOAL>(MeasurableEquiv.vadd c).symm = MeasurableEquiv.vadd (-c)
<VAR>G₀ : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G₀<VAR>MeasurableSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>MeasurableSMul G₀ α<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>⇑(MeasurableEquiv.smul₀ c hc) = fun x => c • x
<VAR>G₀ : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G₀<VAR>MeasurableSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>MeasurableSMul G₀ α<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>(MeasurableEquiv.smul₀ c hc).symm = MeasurableEquiv.smul₀ c⁻¹ ⋯
<VAR>G₀ : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G₀<VAR>MeasurableSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>MeasurableSMul G₀ α<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>MeasurableEmbedding fun x => c • x
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>g : G<GOAL>⇑(MeasurableEquiv.mulLeft g) = fun x => g * x
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>g : G<GOAL>⇑(MeasurableEquiv.addLeft g) = fun x => g + x
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>g : G<GOAL>(MeasurableEquiv.mulLeft g).symm = MeasurableEquiv.mulLeft g⁻¹
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>g : G<GOAL>(MeasurableEquiv.addLeft g).symm = MeasurableEquiv.addLeft (-g)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>g : G<GOAL>(MeasurableEquiv.addLeft g).toEquiv = Equiv.addLeft g
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>g : G<GOAL>(MeasurableEquiv.mulLeft g).toEquiv = Equiv.mulLeft g
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>g : G<GOAL>MeasurableEmbedding fun x => g * x
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>g : G<GOAL>MeasurableEmbedding fun x => g + x
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>g : G<GOAL>MeasurableEmbedding fun x => x * g
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>g : G<GOAL>MeasurableEmbedding fun x => x + g
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>g : G<GOAL>⇑(MeasurableEquiv.mulRight g) = fun x => x * g
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>g : G<GOAL>⇑(MeasurableEquiv.addRight g) = fun x => x + g
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>g : G<GOAL>(MeasurableEquiv.mulRight g).symm = MeasurableEquiv.mulRight g⁻¹
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>g : G<GOAL>(MeasurableEquiv.addRight g).symm = MeasurableEquiv.addRight (-g)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>g : G<GOAL>(MeasurableEquiv.addRight g).toEquiv = Equiv.addRight g
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>g : G<GOAL>(MeasurableEquiv.mulRight g).toEquiv = Equiv.mulRight g
<VAR>G₀ : Type u_2<VAR>MeasurableSpace G₀<VAR>GroupWithZero G₀<VAR>MeasurableMul G₀<VAR>g : G₀<VAR>hg : g ≠ 0<GOAL>MeasurableEmbedding fun x => g * x
<VAR>G₀ : Type u_2<VAR>MeasurableSpace G₀<VAR>GroupWithZero G₀<VAR>MeasurableMul G₀<VAR>g : G₀<VAR>hg : g ≠ 0<GOAL>⇑(MeasurableEquiv.mulLeft₀ g hg) = fun x => g * x
<VAR>G₀ : Type u_2<VAR>MeasurableSpace G₀<VAR>GroupWithZero G₀<VAR>MeasurableMul G₀<VAR>g : G₀<VAR>hg : g ≠ 0<GOAL>(MeasurableEquiv.mulLeft₀ g hg).symm = MeasurableEquiv.mulLeft₀ g⁻¹ ⋯
<VAR>G₀ : Type u_2<VAR>MeasurableSpace G₀<VAR>GroupWithZero G₀<VAR>MeasurableMul G₀<VAR>g : G₀<VAR>hg : g ≠ 0<GOAL>(MeasurableEquiv.mulLeft₀ g hg).toEquiv = Equiv.mulLeft₀ g hg
<VAR>G₀ : Type u_2<VAR>MeasurableSpace G₀<VAR>GroupWithZero G₀<VAR>MeasurableMul G₀<VAR>g : G₀<VAR>hg : g ≠ 0<GOAL>MeasurableEmbedding fun x => x * g
<VAR>G₀ : Type u_2<VAR>MeasurableSpace G₀<VAR>GroupWithZero G₀<VAR>MeasurableMul G₀<VAR>g : G₀<VAR>hg : g ≠ 0<GOAL>⇑(MeasurableEquiv.mulRight₀ g hg) = fun x => x * g
<VAR>G₀ : Type u_2<VAR>MeasurableSpace G₀<VAR>GroupWithZero G₀<VAR>MeasurableMul G₀<VAR>g : G₀<VAR>hg : g ≠ 0<GOAL>(MeasurableEquiv.mulRight₀ g hg).symm = MeasurableEquiv.mulRight₀ g⁻¹ ⋯
<VAR>G₀ : Type u_2<VAR>MeasurableSpace G₀<VAR>GroupWithZero G₀<VAR>MeasurableMul G₀<VAR>g : G₀<VAR>hg : g ≠ 0<GOAL>(MeasurableEquiv.mulRight₀ g hg).toEquiv = Equiv.mulRight₀ g hg
<VAR>G : Type u_4<VAR>MeasurableSpace G<VAR>InvolutiveInv G<VAR>MeasurableInv G<GOAL>(MeasurableEquiv.inv G).toEquiv = Equiv.inv G
<VAR>G : Type u_4<VAR>MeasurableSpace G<VAR>InvolutiveNeg G<VAR>MeasurableNeg G<GOAL>⇑(MeasurableEquiv.neg G) = Neg.neg
<VAR>G : Type u_4<VAR>MeasurableSpace G<VAR>InvolutiveNeg G<VAR>MeasurableNeg G<GOAL>(MeasurableEquiv.neg G).toEquiv = Equiv.neg G
<VAR>G : Type u_4<VAR>MeasurableSpace G<VAR>InvolutiveInv G<VAR>MeasurableInv G<GOAL>⇑(MeasurableEquiv.inv G) = Inv.inv
<VAR>G : Type u_4<VAR>MeasurableSpace G<VAR>InvolutiveInv G<VAR>MeasurableInv G<GOAL>(MeasurableEquiv.inv G).symm = MeasurableEquiv.inv G
<VAR>G : Type u_4<VAR>MeasurableSpace G<VAR>InvolutiveNeg G<VAR>MeasurableNeg G<GOAL>(MeasurableEquiv.neg G).symm = MeasurableEquiv.neg G
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>μ : MeasureTheory.OuterMeasure X<VAR>hm : μ.IsMetric<VAR>I : Finset ι<VAR>s : ι → Set X<VAR>hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → IsMetricSeparated (s i) (s j)<GOAL>μ (⋃ i ∈ I, s i) = ∑ i ∈ I, μ (s i)
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>μ : MeasureTheory.OuterMeasure X<VAR>hm : μ.IsMetric<GOAL>borel X ≤ μ.caratheodory
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>μ : MeasureTheory.OuterMeasure X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>hm : μ.IsMetric<GOAL>inst✝ ≤ μ.caratheodory
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>m : Set X → ℝ≥0∞<VAR>r : ℝ≥0∞<VAR>μ : MeasureTheory.OuterMeasure X<GOAL>μ ≤ MeasureTheory.OuterMeasure.mkMetric'.pre m r ↔ ∀ (s : Set X), EMetric.diam s ≤ r → μ s ≤ m s
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>m : Set X → ℝ≥0∞<VAR>r : ℝ≥0∞<VAR>s : Set X<VAR>hs : EMetric.diam s ≤ r<GOAL>(MeasureTheory.OuterMeasure.mkMetric'.pre m r) s ≤ m s
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>m : Set X → ℝ≥0∞<VAR>r r' : ℝ≥0∞<VAR>h : r ≤ r'<GOAL>MeasureTheory.OuterMeasure.mkMetric'.pre m r' ≤ MeasureTheory.OuterMeasure.mkMetric'.pre m r
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>m : Set X → ℝ≥0∞<GOAL>Monotone fun k => MeasureTheory.OuterMeasure.mkMetric'.pre m (↑k)⁻¹
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>m : Set X → ℝ≥0∞<VAR>s : Set X<GOAL>Filter.Tendsto (fun r => (MeasureTheory.OuterMeasure.mkMetric'.pre m r) s) (𝓝[>] 0) (𝓝 ((MeasureTheory.OuterMeasure.mkMetric' m) s))
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>m : Set X → ℝ≥0∞<VAR>s : Set X<GOAL>Filter.Tendsto (fun n => (MeasureTheory.OuterMeasure.mkMetric'.pre m (↑n)⁻¹) s) Filter.atTop (𝓝 ((MeasureTheory.OuterMeasure.mkMetric' m) s))
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>m : Set X → ℝ≥0∞<GOAL>MeasureTheory.OuterMeasure.mkMetric' m = ⨆ n, MeasureTheory.OuterMeasure.mkMetric'.pre m (↑n)⁻¹
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>OpensMeasurableSpace X<VAR>m : Set X → ℝ≥0∞<VAR>hcl : ∀ (s : Set X), m (closure s) = m s<VAR>r : ℝ≥0∞<GOAL>(MeasureTheory.OuterMeasure.mkMetric'.pre m r).trim = MeasureTheory.OuterMeasure.mkMetric'.pre m r
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>m : Set X → ℝ≥0∞<GOAL>(MeasureTheory.OuterMeasure.mkMetric' m).IsMetric
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>m₁ m₂ : ℝ≥0∞ → ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>h0 : c ≠ 0<VAR>hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂<GOAL>MeasureTheory.OuterMeasure.mkMetric m₁ ≤ c • MeasureTheory.OuterMeasure.mkMetric m₂
<VAR>X : Type u_2<VAR>EMetricSpace X<GOAL>(MeasureTheory.OuterMeasure.mkMetric fun x => ⊤) = ⊤
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>m₁ m₂ : ℝ≥0∞ → ℝ≥0∞<VAR>hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂<GOAL>MeasureTheory.OuterMeasure.mkMetric m₁ ≤ MeasureTheory.OuterMeasure.mkMetric m₂
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>f : X → Y<VAR>hf : Isometry f<VAR>H : Monotone m ∨ Function.Surjective f<GOAL>(MeasureTheory.OuterMeasure.comap f) (MeasureTheory.OuterMeasure.mkMetric m) = MeasureTheory.OuterMeasure.mkMetric m
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>hc' : c ≠ 0<GOAL>MeasureTheory.OuterMeasure.mkMetric (c • m) = c • MeasureTheory.OuterMeasure.mkMetric m
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<GOAL>MeasureTheory.OuterMeasure.mkMetric (c • m) = c • MeasureTheory.OuterMeasure.mkMetric m
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>f : X → Y<VAR>hf : Isometry f<VAR>H : Monotone m ∨ Function.Surjective f<GOAL>(MeasureTheory.OuterMeasure.map f) (MeasureTheory.OuterMeasure.mkMetric m) = (MeasureTheory.OuterMeasure.restrict (Set.range f)) (MeasureTheory.OuterMeasure.mkMetric m)
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>f : X ≃ᵢ Y<GOAL>(MeasureTheory.OuterMeasure.comap ⇑f) (MeasureTheory.OuterMeasure.mkMetric m) = MeasureTheory.OuterMeasure.mkMetric m