G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
this : chaar K₀ K ∈ (fun K => Icc 0 ↑(index ↑K ↑K₀)) K
⊢ 0 ≤ chaar K₀ K
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
⊢ 0 ≤ chaar K₀ K
have := chaar_mem_haarProduct K₀ K (mem_univ _)
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
this : 0 ≤ chaar K₀ K ∧ chaar K₀ K ≤ ↑(index ↑K ↑K₀)
⊢ 0 ≤ chaar K₀ K
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
this : chaar K₀ K ∈ (fun K => Icc 0 ↑(index ↑K ↑K₀)) K
⊢ 0 ≤ chaar K₀ K
rw [mem_Icc] at this
no goals
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
this : 0 ≤ chaar K₀ K ∧ chaar K₀ K ≤ ↑(index ↑K ↑K₀)
⊢ 0 ≤ chaar K₀ K
exact this.1