ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>f : α → β<VAR>Zero β<VAR>hst : s =ᵐ[μ] t<GOAL>s.indicator f =ᵐ[μ] t.indicator f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → β<VAR>Zero β<VAR>hs : μ s = 0<GOAL>s.indicator f =ᵐ[μ] 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → β<VAR>Zero β<VAR>g : α → β<VAR>hs : MeasurableSet s<GOAL>f =ᵐ[μ.restrict s] g ↔ s.indicator f =ᵐ[μ] s.indicator g
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Add G<VAR>μ : MeasureTheory.Measure G<VAR>self : μ.IsAddLeftInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.map (fun x => g + x) μ = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Mul G<VAR>μ : MeasureTheory.Measure G<VAR>self : μ.IsMulLeftInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.map (fun x => g * x) μ = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Add G<VAR>μ : MeasureTheory.Measure G<VAR>self : μ.IsAddRightInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.map (fun x => x + g) μ = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Mul G<VAR>μ : MeasureTheory.Measure G<VAR>self : μ.IsMulRightInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.map (fun x => x * g) μ = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Add G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddLeftInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.map (fun x => g + x) μ = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Mul G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulLeftInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.map (fun x => g * x) μ = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Add G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddRightInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.map (fun x => x + g) μ = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Mul G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulRightInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.map (fun x => x * g) μ = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Mul G<VAR>MeasurableMul G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulLeftInvariant<VAR>g : G<GOAL>MeasureTheory.MeasurePreserving (fun x => g * x) μ μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Add G<VAR>MeasurableAdd G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddLeftInvariant<VAR>g : G<GOAL>MeasureTheory.MeasurePreserving (fun x => g + x) μ μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Mul G<VAR>MeasurableMul G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulLeftInvariant<VAR>g : G<VAR>X : Type u_4<VAR>MeasurableSpace X<VAR>μ' : MeasureTheory.Measure X<VAR>f : X → G<VAR>hf : MeasureTheory.MeasurePreserving f μ' μ<GOAL>MeasureTheory.MeasurePreserving (fun x => g * f x) μ' μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Add G<VAR>MeasurableAdd G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddLeftInvariant<VAR>g : G<VAR>X : Type u_4<VAR>MeasurableSpace X<VAR>μ' : MeasureTheory.Measure X<VAR>f : X → G<VAR>hf : MeasureTheory.MeasurePreserving f μ' μ<GOAL>MeasureTheory.MeasurePreserving (fun x => g + f x) μ' μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Add G<VAR>MeasurableAdd G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddRightInvariant<VAR>g : G<GOAL>MeasureTheory.MeasurePreserving (fun x => x + g) μ μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Mul G<VAR>MeasurableMul G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulRightInvariant<VAR>g : G<GOAL>MeasureTheory.MeasurePreserving (fun x => x * g) μ μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Mul G<VAR>MeasurableMul G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulRightInvariant<VAR>g : G<VAR>X : Type u_4<VAR>MeasurableSpace X<VAR>μ' : MeasureTheory.Measure X<VAR>f : X → G<VAR>hf : MeasureTheory.MeasurePreserving f μ' μ<GOAL>MeasureTheory.MeasurePreserving (fun x => f x * g) μ' μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Add G<VAR>MeasurableAdd G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddRightInvariant<VAR>g : G<VAR>X : Type u_4<VAR>MeasurableSpace X<VAR>μ' : MeasureTheory.Measure X<VAR>f : X → G<VAR>hf : MeasureTheory.MeasurePreserving f μ' μ<GOAL>MeasureTheory.MeasurePreserving (fun x => f x + g) μ' μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Add G<VAR>MeasurableAdd G<VAR>μ : MeasureTheory.Measure G<GOAL>(∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => g + h) ⁻¹' A) = μ A) ↔ μ.IsAddLeftInvariant
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Mul G<VAR>MeasurableMul G<VAR>μ : MeasureTheory.Measure G<GOAL>(∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => g * h) ⁻¹' A) = μ A) ↔ μ.IsMulLeftInvariant
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Add G<VAR>MeasurableAdd G<VAR>μ : MeasureTheory.Measure G<GOAL>(∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => h + g) ⁻¹' A) = μ A) ↔ μ.IsAddRightInvariant
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Mul G<VAR>MeasurableMul G<VAR>μ : MeasureTheory.Measure G<GOAL>(∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => h * g) ⁻¹' A) = μ A) ↔ μ.IsMulRightInvariant
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Add G<VAR>μ : MeasureTheory.Measure G<VAR>MeasurableAdd G<VAR>H : Type u_4<VAR>MeasurableSpace H<VAR>Add H<VAR>MeasurableAdd H<VAR>μ.IsAddLeftInvariant<VAR>f : AddHom G H<VAR>hf : Measurable ⇑f<VAR>h_surj : Function.Surjective ⇑f<GOAL>(MeasureTheory.Measure.map (⇑f) μ).IsAddLeftInvariant
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Mul G<VAR>μ : MeasureTheory.Measure G<VAR>MeasurableMul G<VAR>H : Type u_4<VAR>MeasurableSpace H<VAR>Mul H<VAR>MeasurableMul H<VAR>μ.IsMulLeftInvariant<VAR>f : G →ₙ* H<VAR>hf : Measurable ⇑f<VAR>h_surj : Function.Surjective ⇑f<GOAL>(MeasureTheory.Measure.map (⇑f) μ).IsMulLeftInvariant
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Semigroup G<VAR>MeasurableMul G<VAR>μ : MeasureTheory.Measure G<VAR>α : Type u_4<VAR>SMul α G<VAR>SMulCommClass α G G<VAR>MeasurableSpace α<VAR>MeasurableSMul α G<VAR>μ.IsMulLeftInvariant<VAR>a : α<GOAL>(MeasureTheory.Measure.map (fun x => a • x) μ).IsMulLeftInvariant
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddSemigroup G<VAR>MeasurableAdd G<VAR>μ : MeasureTheory.Measure G<VAR>α : Type u_4<VAR>VAdd α G<VAR>VAddCommClass α G G<VAR>MeasurableSpace α<VAR>MeasurableVAdd α G<VAR>μ.IsAddLeftInvariant<VAR>a : α<GOAL>(MeasureTheory.Measure.map (fun x => a +ᵥ x) μ).IsAddLeftInvariant
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddSemigroup G<VAR>MeasurableAdd G<VAR>μ : MeasureTheory.Measure G<VAR>α : Type u_4<VAR>VAdd α G<VAR>VAddCommClass α Gᵃᵒᵖ G<VAR>MeasurableSpace α<VAR>MeasurableVAdd α G<VAR>μ.IsAddRightInvariant<VAR>a : α<GOAL>(MeasureTheory.Measure.map (fun x => a +ᵥ x) μ).IsAddRightInvariant
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Semigroup G<VAR>MeasurableMul G<VAR>μ : MeasureTheory.Measure G<VAR>α : Type u_4<VAR>SMul α G<VAR>SMulCommClass α Gᵐᵒᵖ G<VAR>MeasurableSpace α<VAR>MeasurableSMul α G<VAR>μ.IsMulRightInvariant<VAR>a : α<GOAL>(MeasureTheory.Measure.map (fun x => a • x) μ).IsMulRightInvariant
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>DivInvMonoid G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulRightInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.map (fun x => x / g) μ = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>SubNegMonoid G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddRightInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.map (fun x => x - g) μ = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddRightInvariant<VAR>g : G<GOAL>MeasureTheory.MeasurePreserving (fun x => x - g) μ μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulRightInvariant<VAR>g : G<GOAL>MeasureTheory.MeasurePreserving (fun x => x / g) μ μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddLeftInvariant<VAR>g : G<VAR>A : Set G<GOAL>μ ((fun h => g + h) ⁻¹' A) = μ A
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulLeftInvariant<VAR>g : G<VAR>A : Set G<GOAL>μ ((fun h => g * h) ⁻¹' A) = μ A
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulRightInvariant<VAR>g : G<VAR>A : Set G<GOAL>μ ((fun h => h * g) ⁻¹' A) = μ A
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddRightInvariant<VAR>g : G<VAR>A : Set G<GOAL>μ ((fun h => h + g) ⁻¹' A) = μ A
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulLeftInvariant<VAR>x : G<GOAL>Filter.map (fun h => x * h) (MeasureTheory.ae μ) = MeasureTheory.ae μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddLeftInvariant<VAR>x : G<GOAL>Filter.map (fun h => x + h) (MeasureTheory.ae μ) = MeasureTheory.ae μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddRightInvariant<VAR>x : G<GOAL>Filter.map (fun h => h + x) (MeasureTheory.ae μ) = MeasureTheory.ae μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulRightInvariant<VAR>x : G<GOAL>Filter.map (fun h => h * x) (MeasureTheory.ae μ) = MeasureTheory.ae μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulRightInvariant<VAR>x : G<GOAL>Filter.map (fun t => t / x) (MeasureTheory.ae μ) = MeasureTheory.ae μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddRightInvariant<VAR>x : G<GOAL>Filter.map (fun t => t - x) (MeasureTheory.ae μ) = MeasureTheory.ae μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddLeftInvariant<VAR>t : G<VAR>p : G → Prop<GOAL>(∀ᵐ (x : G) ∂μ, p (t + x)) ↔ ∀ᵐ (x : G) ∂μ, p x
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulLeftInvariant<VAR>t : G<VAR>p : G → Prop<GOAL>(∀ᵐ (x : G) ∂μ, p (t * x)) ↔ ∀ᵐ (x : G) ∂μ, p x
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddRightInvariant<VAR>t : G<VAR>p : G → Prop<GOAL>(∀ᵐ (x : G) ∂μ, p (x + t)) ↔ ∀ᵐ (x : G) ∂μ, p x
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulRightInvariant<VAR>t : G<VAR>p : G → Prop<GOAL>(∀ᵐ (x : G) ∂μ, p (x * t)) ↔ ∀ᵐ (x : G) ∂μ, p x
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddRightInvariant<VAR>t : G<VAR>p : G → Prop<GOAL>(∀ᵐ (x : G) ∂μ, p (x - t)) ↔ ∀ᵐ (x : G) ∂μ, p x
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulRightInvariant<VAR>t : G<VAR>p : G → Prop<GOAL>(∀ᵐ (x : G) ∂μ, p (x / t)) ↔ ∀ᵐ (x : G) ∂μ, p x
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Neg G<VAR>μ : MeasureTheory.Measure G<VAR>self : μ.IsNegInvariant<GOAL>μ.neg = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Inv G<VAR>μ : MeasureTheory.Measure G<VAR>self : μ.IsInvInvariant<GOAL>μ.inv = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Neg G<VAR>μ : MeasureTheory.Measure G<GOAL>μ.neg = MeasureTheory.Measure.map Neg.neg μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Inv G<VAR>μ : MeasureTheory.Measure G<GOAL>μ.inv = MeasureTheory.Measure.map Inv.inv μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Inv G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsInvInvariant<GOAL>μ.inv = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Neg G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsNegInvariant<GOAL>μ.neg = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Inv G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsInvInvariant<GOAL>MeasureTheory.Measure.map Inv.inv μ = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Neg G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsNegInvariant<GOAL>MeasureTheory.Measure.map Neg.neg μ = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Neg G<VAR>MeasurableNeg G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsNegInvariant<GOAL>MeasureTheory.MeasurePreserving Neg.neg μ μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Inv G<VAR>MeasurableInv G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsInvInvariant<GOAL>MeasureTheory.MeasurePreserving Inv.inv μ μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>InvolutiveNeg G<VAR>MeasurableNeg G<VAR>μ : MeasureTheory.Measure G<VAR>s : Set G<GOAL>μ.neg s = μ (-s)
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>InvolutiveInv G<VAR>MeasurableInv G<VAR>μ : MeasureTheory.Measure G<VAR>s : Set G<GOAL>μ.inv s = μ s⁻¹
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>InvolutiveNeg G<VAR>MeasurableNeg G<VAR>μ : MeasureTheory.Measure G<GOAL>μ.neg.neg = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>InvolutiveInv G<VAR>MeasurableInv G<VAR>μ : MeasureTheory.Measure G<GOAL>μ.inv.inv = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>InvolutiveNeg G<VAR>MeasurableNeg G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsNegInvariant<VAR>A : Set G<GOAL>μ (-A) = μ A
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>InvolutiveInv G<VAR>MeasurableInv G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsInvInvariant<VAR>A : Set G<GOAL>μ A⁻¹ = μ A
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>InvolutiveNeg G<VAR>MeasurableNeg G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsNegInvariant<VAR>A : Set G<GOAL>μ (Neg.neg ⁻¹' A) = μ A
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>InvolutiveInv G<VAR>MeasurableInv G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsInvInvariant<VAR>A : Set G<GOAL>μ (Inv.inv ⁻¹' A) = μ A
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>SubtractionMonoid G<VAR>MeasurableAdd G<VAR>MeasurableNeg G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsNegInvariant<VAR>μ.IsAddLeftInvariant<VAR>g : G<GOAL>MeasureTheory.MeasurePreserving (fun t => g - t) μ μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>DivisionMonoid G<VAR>MeasurableMul G<VAR>MeasurableInv G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsInvInvariant<VAR>μ.IsMulLeftInvariant<VAR>g : G<GOAL>MeasureTheory.MeasurePreserving (fun t => g / t) μ μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>SubtractionMonoid G<VAR>MeasurableAdd G<VAR>MeasurableNeg G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsNegInvariant<VAR>μ.IsAddLeftInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.map (fun t => g - t) μ = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>DivisionMonoid G<VAR>MeasurableMul G<VAR>MeasurableInv G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsInvInvariant<VAR>μ.IsMulLeftInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.map (fun t => g / t) μ = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>SubtractionMonoid G<VAR>MeasurableAdd G<VAR>MeasurableNeg G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsNegInvariant<VAR>μ.IsAddLeftInvariant<VAR>g : G<GOAL>MeasureTheory.MeasurePreserving (fun t => -(g + t)) μ μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>DivisionMonoid G<VAR>MeasurableMul G<VAR>MeasurableInv G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsInvInvariant<VAR>μ.IsMulLeftInvariant<VAR>g : G<GOAL>MeasureTheory.MeasurePreserving (fun t => (g * t)⁻¹) μ μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>DivisionMonoid G<VAR>MeasurableMul G<VAR>MeasurableInv G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsInvInvariant<VAR>μ.IsMulLeftInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.map (fun t => (g * t)⁻¹) μ = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>SubtractionMonoid G<VAR>MeasurableAdd G<VAR>MeasurableNeg G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsNegInvariant<VAR>μ.IsAddLeftInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.map (fun t => -(g + t)) μ = μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul G<VAR>MeasurableInv G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulLeftInvariant<VAR>μ.IsInvInvariant<VAR>x : G<GOAL>Filter.map (fun t => x / t) (MeasureTheory.ae μ) = MeasureTheory.ae μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>MeasurableNeg G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddLeftInvariant<VAR>μ.IsNegInvariant<VAR>x : G<GOAL>Filter.map (fun t => x - t) (MeasureTheory.ae μ) = MeasureTheory.ae μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>TopologicalAddGroup G<GOAL>μ.neg.Regular ↔ μ.Regular
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>TopologicalGroup G<GOAL>μ.inv.Regular ↔ μ.Regular
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>TopologicalGroup G<GOAL>μ.inv.InnerRegular ↔ μ.InnerRegular
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>TopologicalAddGroup G<GOAL>μ.neg.InnerRegular ↔ μ.InnerRegular
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>LocallyCompactSpace G<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>μ.InnerRegularCompactLTTop<VAR>k : Set G<VAR>hk : IsCompact k<VAR>h'k : IsClosed k<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∀ᶠ (g : G) in 𝓝 0, μ ((g +ᵥ k) \ k) < ε
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>TopologicalGroup G<VAR>LocallyCompactSpace G<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>μ.InnerRegularCompactLTTop<VAR>k : Set G<VAR>hk : IsCompact k<VAR>h'k : IsClosed k<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∀ᶠ (g : G) in 𝓝 1, μ (g • k \ k) < ε
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>TopologicalGroup G<VAR>LocallyCompactSpace G<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>μ.InnerRegularCompactLTTop<VAR>k : Set G<VAR>hk : IsCompact k<VAR>h'k : IsClosed k<GOAL>Filter.Tendsto (fun g => μ (g • k \ k)) (𝓝 1) (𝓝 0)
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>LocallyCompactSpace G<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>μ.InnerRegularCompactLTTop<VAR>k : Set G<VAR>hk : IsCompact k<VAR>h'k : IsClosed k<GOAL>Filter.Tendsto (fun g => μ ((g +ᵥ k) \ k)) (𝓝 0) (𝓝 0)
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>TopologicalGroup G<VAR>μ.IsMulLeftInvariant<VAR>K : Set G<VAR>hK : IsCompact K<VAR>h : μ K ≠ 0<GOAL>μ.IsOpenPosMeasure
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>μ.IsAddLeftInvariant<VAR>K : Set G<VAR>hK : IsCompact K<VAR>h : μ K ≠ 0<GOAL>μ.IsOpenPosMeasure
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>TopologicalGroup G<VAR>μ.IsMulLeftInvariant<VAR>μ.Regular<VAR>s : Set G<VAR>hs : IsOpen s<GOAL>μ s = 0 ↔ s = ∅ ∨ μ = 0
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>μ.IsAddLeftInvariant<VAR>μ.Regular<VAR>s : Set G<VAR>hs : IsOpen s<GOAL>μ s = 0 ↔ s = ∅ ∨ μ = 0
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>μ.IsAddLeftInvariant<VAR>μ.Regular<VAR>hμ : μ ≠ 0<VAR>s : Set G<VAR>hs : IsOpen s<GOAL>μ s ≠ 0 ↔ s.Nonempty
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>TopologicalGroup G<VAR>μ.IsMulLeftInvariant<VAR>μ.Regular<VAR>hμ : μ ≠ 0<VAR>s : Set G<VAR>hs : IsOpen s<GOAL>μ s ≠ 0 ↔ s.Nonempty
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>μ.IsAddLeftInvariant<VAR>μ.Regular<VAR>h3μ : μ ≠ 0<VAR>s : Set G<VAR>hs : IsOpen s<GOAL>0 < μ s ↔ s.Nonempty
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>TopologicalGroup G<VAR>μ.IsMulLeftInvariant<VAR>μ.Regular<VAR>h3μ : μ ≠ 0<VAR>s : Set G<VAR>hs : IsOpen s<GOAL>0 < μ s ↔ s.Nonempty
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>μ.IsAddLeftInvariant<VAR>U : Set G<VAR>hU : IsOpen U<VAR>h'U : U.Nonempty<VAR>h : μ U ≠ ⊤<VAR>K : Set G<VAR>hK : IsCompact K<GOAL>μ K < ⊤
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>TopologicalGroup G<VAR>μ.IsMulLeftInvariant<VAR>U : Set G<VAR>hU : IsOpen U<VAR>h'U : U.Nonempty<VAR>h : μ U ≠ ⊤<VAR>K : Set G<VAR>hK : IsCompact K<GOAL>μ K < ⊤
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>TopologicalGroup G<VAR>μ.IsMulLeftInvariant<VAR>U : Set G<VAR>hU : (interior U).Nonempty<VAR>h : μ U ≠ ⊤<VAR>K : Set G<VAR>hK : IsCompact K<GOAL>μ K < ⊤
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>μ.IsAddLeftInvariant<VAR>U : Set G<VAR>hU : (interior U).Nonempty<VAR>h : μ U ≠ ⊤<VAR>K : Set G<VAR>hK : IsCompact K<GOAL>μ K < ⊤
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>WeaklyLocallyCompactSpace G<VAR>NoncompactSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsOpenPosMeasure<VAR>μ.IsMulLeftInvariant<GOAL>μ Set.univ = ⊤
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>WeaklyLocallyCompactSpace G<VAR>NoncompactSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsOpenPosMeasure<VAR>μ.IsAddLeftInvariant<GOAL>μ Set.univ = ⊤
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>s * closure {1} = s
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>s + closure {0} = s
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>k s : Set G<VAR>hk : IsCompact k<VAR>hs : MeasurableSet s<VAR>h : k ⊆ s<GOAL>closure k ⊆ s
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>k s : Set G<VAR>hk : IsCompact k<VAR>hs : MeasurableSet s<VAR>h : k ⊆ s<GOAL>closure k ⊆ s
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>s : Set G<VAR>μ : MeasureTheory.Measure G<GOAL>μ (s * closure {1}) = μ s
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>s : Set G<VAR>μ : MeasureTheory.Measure G<GOAL>μ (s + closure {0}) = μ s
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>k : Set G<VAR>hk : IsCompact k<VAR>μ : MeasureTheory.Measure G<GOAL>μ (closure k) = μ k
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>k : Set G<VAR>hk : IsCompact k<VAR>μ : MeasureTheory.Measure G<GOAL>μ (closure k) = μ k
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>h : μ.InnerRegularCompactLTTop<GOAL>μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) fun s => MeasurableSet s ∧ μ s ≠ ⊤
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>TopologicalGroup G<VAR>h : μ.InnerRegularCompactLTTop<GOAL>μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) fun s => MeasurableSet s ∧ μ s ≠ ⊤
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Group G<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>TopologicalGroup G<VAR>BorelSpace G<VAR>g : G<GOAL>μ {g} = μ {1}