ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<GOAL>MeasureTheory.Measure.haar.prehaar (↑K₀) U ⊥ = 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>K : TopologicalSpace.Compacts G<GOAL>0 ≤ MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>K : TopologicalSpace.Compacts G<GOAL>0 ≤ MeasureTheory.Measure.haar.prehaar (↑K₀) U K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>K₀ : Set G<VAR>f : TopologicalSpace.Compacts G → ℝ<GOAL>f ∈ MeasureTheory.Measure.haar.addHaarProduct K₀ ↔ ∀ (K : TopologicalSpace.Compacts G), f K ∈ Set.Icc 0 ↑(MeasureTheory.Measure.haar.addIndex (↑K) K₀)
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>K₀ : Set G<VAR>f : TopologicalSpace.Compacts G → ℝ<GOAL>f ∈ MeasureTheory.Measure.haar.haarProduct K₀ ↔ ∀ (K : TopologicalSpace.Compacts G), f K ∈ Set.Icc 0 ↑(MeasureTheory.Measure.haar.index (↑K) K₀)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K V : Set G<VAR>hK : IsCompact K<VAR>hV : (interior V).Nonempty<GOAL>∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g + h) ⁻¹' V}
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K V : Set G<VAR>hK : IsCompact K<VAR>hV : (interior V).Nonempty<GOAL>∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K V : Set G<VAR>hK : IsCompact K<VAR>hV : (interior V).Nonempty<GOAL>∃ t, K ⊆ ⋃ g ∈ t, (fun h => g + h) ⁻¹' V ∧ t.card = MeasureTheory.Measure.haar.addIndex K V
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K V : Set G<VAR>hK : IsCompact K<VAR>hV : (interior V).Nonempty<GOAL>∃ t, K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V ∧ t.card = MeasureTheory.Measure.haar.index K V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>K : TopologicalSpace.Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>MeasureTheory.Measure.haar.addIndex (↑K) V ≤ MeasureTheory.Measure.haar.addIndex ↑K ↑K₀ * MeasureTheory.Measure.haar.addIndex (↑K₀) V
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>K : TopologicalSpace.Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>MeasureTheory.Measure.haar.index (↑K) V ≤ MeasureTheory.Measure.haar.index ↑K ↑K₀ * MeasureTheory.Measure.haar.index (↑K₀) V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K : TopologicalSpace.PositiveCompacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>0 < MeasureTheory.Measure.haar.addIndex (↑K) V
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K : TopologicalSpace.PositiveCompacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>0 < MeasureTheory.Measure.haar.index (↑K) V
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K K' V : Set G<VAR>hK' : IsCompact K'<VAR>h : K ⊆ K'<VAR>hV : (interior V).Nonempty<GOAL>MeasureTheory.Measure.haar.index K V ≤ MeasureTheory.Measure.haar.index K' V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K K' V : Set G<VAR>hK' : IsCompact K'<VAR>h : K ⊆ K'<VAR>hV : (interior V).Nonempty<GOAL>MeasureTheory.Measure.haar.addIndex K V ≤ MeasureTheory.Measure.haar.addIndex K' V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>MeasureTheory.Measure.haar.addIndex (K₁.carrier ∪ K₂.carrier) V ≤ MeasureTheory.Measure.haar.addIndex K₁.carrier V + MeasureTheory.Measure.haar.addIndex K₂.carrier V
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>MeasureTheory.Measure.haar.index (K₁.carrier ∪ K₂.carrier) V ≤ MeasureTheory.Measure.haar.index K₁.carrier V + MeasureTheory.Measure.haar.index K₂.carrier V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>h : Disjoint (K₁.carrier + -V) (K₂.carrier + -V)<GOAL>MeasureTheory.Measure.haar.addIndex (K₁.carrier ∪ K₂.carrier) V = MeasureTheory.Measure.haar.addIndex K₁.carrier V + MeasureTheory.Measure.haar.addIndex K₂.carrier V
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)<GOAL>MeasureTheory.Measure.haar.index (K₁.carrier ∪ K₂.carrier) V = MeasureTheory.Measure.haar.index K₁.carrier V + MeasureTheory.Measure.haar.index K₂.carrier V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>g : G<GOAL>MeasureTheory.Measure.haar.addIndex ((fun h => g + h) '' K) V ≤ MeasureTheory.Measure.haar.addIndex K V
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>g : G<GOAL>MeasureTheory.Measure.haar.index ((fun h => g * h) '' K) V ≤ MeasureTheory.Measure.haar.index K V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>g : G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>MeasureTheory.Measure.haar.addIndex ((fun h => g + h) '' K) V = MeasureTheory.Measure.haar.addIndex K V
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>g : G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>MeasureTheory.Measure.haar.index ((fun h => g * h) '' K) V = MeasureTheory.Measure.haar.index K V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>K : TopologicalSpace.Compacts G<VAR>hU : (interior U).Nonempty<GOAL>MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K ≤ ↑(MeasureTheory.Measure.haar.addIndex ↑K ↑K₀)
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>K : TopologicalSpace.Compacts G<VAR>hU : (interior U).Nonempty<GOAL>MeasureTheory.Measure.haar.prehaar (↑K₀) U K ≤ ↑(MeasureTheory.Measure.haar.index ↑K ↑K₀)
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<VAR>K : Set G<VAR>h1K : IsCompact K<VAR>h2K : (interior K).Nonempty<GOAL>0 < MeasureTheory.Measure.haar.prehaar (↑K₀) U { carrier := K, isCompact' := h1K }
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<VAR>K : Set G<VAR>h1K : IsCompact K<VAR>h2K : (interior K).Nonempty<GOAL>0 < MeasureTheory.Measure.haar.addPrehaar (↑K₀) U { carrier := K, isCompact' := h1K }
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<VAR>K₁ K₂ : TopologicalSpace.Compacts G<VAR>h : ↑K₁ ⊆ K₂.carrier<GOAL>MeasureTheory.Measure.haar.prehaar (↑K₀) U K₁ ≤ MeasureTheory.Measure.haar.prehaar (↑K₀) U K₂
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<VAR>K₁ K₂ : TopologicalSpace.Compacts G<VAR>h : ↑K₁ ⊆ K₂.carrier<GOAL>MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₁ ≤ MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₂
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<GOAL>MeasureTheory.Measure.haar.prehaar (↑K₀) U K₀.toCompacts = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<GOAL>MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₀.toCompacts = 1
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<VAR>hU : (interior U).Nonempty<GOAL>MeasureTheory.Measure.haar.prehaar (↑K₀) U (K₁ ⊔ K₂) ≤ MeasureTheory.Measure.haar.prehaar (↑K₀) U K₁ + MeasureTheory.Measure.haar.prehaar (↑K₀) U K₂
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<VAR>hU : (interior U).Nonempty<GOAL>MeasureTheory.Measure.haar.addPrehaar (↑K₀) U (K₁ ⊔ K₂) ≤ MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₁ + MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₂
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<VAR>hU : (interior U).Nonempty<VAR>h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)<GOAL>MeasureTheory.Measure.haar.prehaar (↑K₀) U (K₁ ⊔ K₂) = MeasureTheory.Measure.haar.prehaar (↑K₀) U K₁ + MeasureTheory.Measure.haar.prehaar (↑K₀) U K₂
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<VAR>hU : (interior U).Nonempty<VAR>h : Disjoint (K₁.carrier + -U) (K₂.carrier + -U)<GOAL>MeasureTheory.Measure.haar.addPrehaar (↑K₀) U (K₁ ⊔ K₂) = MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₁ + MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₂
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<VAR>g : G<VAR>K : TopologicalSpace.Compacts G<GOAL>MeasureTheory.Measure.haar.prehaar (↑K₀) U (TopologicalSpace.Compacts.map (fun b => g * b) ⋯ K) = MeasureTheory.Measure.haar.prehaar (↑K₀) U K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<VAR>g : G<VAR>K : TopologicalSpace.Compacts G<GOAL>MeasureTheory.Measure.haar.addPrehaar (↑K₀) U (TopologicalSpace.Compacts.map (fun b => g + b) ⋯ K) = MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<GOAL>MeasureTheory.Measure.haar.addPrehaar (↑K₀) U ∈ MeasureTheory.Measure.haar.addHaarProduct ↑K₀
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<GOAL>MeasureTheory.Measure.haar.prehaar (↑K₀) U ∈ MeasureTheory.Measure.haar.haarProduct ↑K₀
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>(MeasureTheory.Measure.haar.addHaarProduct ↑K₀ ∩ ⋂ V, MeasureTheory.Measure.haar.clAddPrehaar (↑K₀) V).Nonempty
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>(MeasureTheory.Measure.haar.haarProduct ↑K₀ ∩ ⋂ V, MeasureTheory.Measure.haar.clPrehaar (↑K₀) V).Nonempty
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>MeasureTheory.Measure.haar.chaar K₀ ∈ MeasureTheory.Measure.haar.haarProduct ↑K₀
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>MeasureTheory.Measure.haar.addCHaar K₀ ∈ MeasureTheory.Measure.haar.addHaarProduct ↑K₀
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>V : TopologicalSpace.OpenNhdsOf 1<GOAL>MeasureTheory.Measure.haar.chaar K₀ ∈ MeasureTheory.Measure.haar.clPrehaar (↑K₀) V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>V : TopologicalSpace.OpenNhdsOf 0<GOAL>MeasureTheory.Measure.haar.addCHaar K₀ ∈ MeasureTheory.Measure.haar.clAddPrehaar (↑K₀) V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>K : TopologicalSpace.Compacts G<GOAL>0 ≤ MeasureTheory.Measure.haar.addCHaar K₀ K
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>K : TopologicalSpace.Compacts G<GOAL>0 ≤ MeasureTheory.Measure.haar.chaar K₀ K
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>MeasureTheory.Measure.haar.chaar K₀ ⊥ = 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>MeasureTheory.Measure.haar.addCHaar K₀ ⊥ = 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>MeasureTheory.Measure.haar.addCHaar K₀ K₀.toCompacts = 1
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>MeasureTheory.Measure.haar.chaar K₀ K₀.toCompacts = 1
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<VAR>h : ↑K₁ ⊆ ↑K₂<GOAL>MeasureTheory.Measure.haar.chaar K₀ K₁ ≤ MeasureTheory.Measure.haar.chaar K₀ K₂
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<VAR>h : ↑K₁ ⊆ ↑K₂<GOAL>MeasureTheory.Measure.haar.addCHaar K₀ K₁ ≤ MeasureTheory.Measure.haar.addCHaar K₀ K₂
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<GOAL>MeasureTheory.Measure.haar.addCHaar K₀ (K₁ ⊔ K₂) ≤ MeasureTheory.Measure.haar.addCHaar K₀ K₁ + MeasureTheory.Measure.haar.addCHaar K₀ K₂
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<GOAL>MeasureTheory.Measure.haar.chaar K₀ (K₁ ⊔ K₂) ≤ MeasureTheory.Measure.haar.chaar K₀ K₁ + MeasureTheory.Measure.haar.chaar K₀ K₂
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<GOAL>MeasureTheory.Measure.haar.chaar K₀ (K₁ ⊔ K₂) = MeasureTheory.Measure.haar.chaar K₀ K₁ + MeasureTheory.Measure.haar.chaar K₀ K₂
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<GOAL>MeasureTheory.Measure.haar.addCHaar K₀ (K₁ ⊔ K₂) = MeasureTheory.Measure.haar.addCHaar K₀ K₁ + MeasureTheory.Measure.haar.addCHaar K₀ K₂
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>g : G<VAR>K : TopologicalSpace.Compacts G<GOAL>MeasureTheory.Measure.haar.chaar K₀ (TopologicalSpace.Compacts.map (fun b => g * b) ⋯ K) = MeasureTheory.Measure.haar.chaar K₀ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>g : G<VAR>K : TopologicalSpace.Compacts G<GOAL>MeasureTheory.Measure.haar.addCHaar K₀ (TopologicalSpace.Compacts.map (fun b => g + b) ⋯ K) = MeasureTheory.Measure.haar.addCHaar K₀ K
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>K : TopologicalSpace.Compacts G<GOAL>(fun s => ↑((MeasureTheory.Measure.haar.haarContent K₀).toFun s)) K = ↑(let_fun this := ⟨MeasureTheory.Measure.haar.chaar K₀ K, ⋯⟩; this)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>K : TopologicalSpace.Compacts G<GOAL>(fun s => ↑((MeasureTheory.Measure.haar.addHaarContent K₀).toFun s)) K = ↑(let_fun this := ⟨MeasureTheory.Measure.haar.addCHaar K₀ K, ⋯⟩; this)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>(fun s => ↑((MeasureTheory.Measure.haar.addHaarContent K₀).toFun s)) K₀.toCompacts = 1
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>(fun s => ↑((MeasureTheory.Measure.haar.haarContent K₀).toFun s)) K₀.toCompacts = 1
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>g : G<VAR>K : TopologicalSpace.Compacts G<GOAL>(fun s => ↑((MeasureTheory.Measure.haar.haarContent K₀).toFun s)) (TopologicalSpace.Compacts.map (fun b => g * b) ⋯ K) = (fun s => ↑((MeasureTheory.Measure.haar.haarContent K₀).toFun s)) K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>g : G<VAR>K : TopologicalSpace.Compacts G<GOAL>(fun s => ↑((MeasureTheory.Measure.haar.addHaarContent K₀).toFun s)) (TopologicalSpace.Compacts.map (fun b => g + b) ⋯ K) = (fun s => ↑((MeasureTheory.Measure.haar.addHaarContent K₀).toFun s)) K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>0 < (MeasureTheory.Measure.haar.addHaarContent K₀).outerMeasure ↑K₀
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>0 < (MeasureTheory.Measure.haar.haarContent K₀).outerMeasure ↑K₀
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>0 < (MeasureTheory.Measure.haar.haarContent K₀).outerMeasure (closure ↑K₀)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>0 < (MeasureTheory.Measure.haar.addHaarContent K₀).outerMeasure (closure ↑K₀)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.Measure.addHaarMeasure K₀) s = (MeasureTheory.Measure.haar.addHaarContent K₀).outerMeasure s / (MeasureTheory.Measure.haar.addHaarContent K₀).measure ↑K₀
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.Measure.haarMeasure K₀) s = (MeasureTheory.Measure.haar.haarContent K₀).outerMeasure s / (MeasureTheory.Measure.haar.haarContent K₀).measure ↑K₀
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>(MeasureTheory.Measure.addHaarMeasure K₀) ↑K₀ = 1
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>(MeasureTheory.Measure.haarMeasure K₀) ↑K₀ = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>(MeasureTheory.Measure.addHaarMeasure K₀) (closure ↑K₀) = 1
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>(MeasureTheory.Measure.haarMeasure K₀) (closure ↑K₀) = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>LocallyCompactSpace G<VAR>μ.InnerRegular<VAR>E : Set G<VAR>hE : MeasurableSet E<VAR>hEpos : 0 < μ E<GOAL>E - E ∈ 𝓝 0
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>LocallyCompactSpace G<VAR>μ.InnerRegular<VAR>E : Set G<VAR>hE : MeasurableSet E<VAR>hEpos : 0 < μ E<GOAL>E / E ∈ 𝓝 1
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>SecondCountableTopology G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ<VAR>μ.IsMulLeftInvariant<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>μ = μ ↑K₀ • MeasureTheory.Measure.haarMeasure K₀
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>SecondCountableTopology G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ<VAR>μ.IsAddLeftInvariant<VAR>K₀ : TopologicalSpace.PositiveCompacts G<GOAL>μ = μ ↑K₀ • MeasureTheory.Measure.addHaarMeasure K₀
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>SecondCountableTopology G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ<VAR>μ.IsAddLeftInvariant<GOAL>MeasureTheory.Measure.addHaarMeasure K₀ = μ ↔ μ ↑K₀ = 1
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>SecondCountableTopology G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ<VAR>μ.IsMulLeftInvariant<GOAL>MeasureTheory.Measure.haarMeasure K₀ = μ ↔ μ ↑K₀ = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>SecondCountableTopology G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ<VAR>μ.IsAddLeftInvariant<VAR>K : Set G<VAR>hK : IsCompact K<VAR>h2K : (interior K).Nonempty<VAR>hμK : μ K ≠ ⊤<GOAL>μ.Regular
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>SecondCountableTopology G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ<VAR>μ.IsMulLeftInvariant<VAR>K : Set G<VAR>hK : IsCompact K<VAR>h2K : (interior K).Nonempty<VAR>hμK : μ K ≠ ⊤<GOAL>μ.Regular
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>μ.everywherePosSubset s ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>∃ u, IsOpen u ∧ μ.everywherePosSubset s = s \ u
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>OpensMeasurableSpace α<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (μ.everywherePosSubset s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : IsClosed s<GOAL>IsClosed (μ.everywherePosSubset s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : IsCompact s<GOAL>IsCompact (μ.everywherePosSubset s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s k : Set α<VAR>hk : IsCompact k<VAR>h'k : k ⊆ s \ μ.everywherePosSubset s<GOAL>μ k = 0