G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : Set.Nonempty (interior U)
⊢ ↑(index (↑K) U) / ↑(index (↑K₀) U) ≤ ↑(index ↑K ↑K₀)
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : Set.Nonempty (interior U)
⊢ prehaar (↑K₀) U K ≤ ↑(index ↑K ↑K₀)
unfold prehaar
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : Set.Nonempty (interior U)
⊢ index (↑K) U ≤ index ↑K ↑K₀ * index (↑K₀) U

G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : Set.Nonempty (interior U)
⊢ 0 < index (↑K₀) U
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : Set.Nonempty (interior U)
⊢ ↑(index (↑K) U) / ↑(index (↑K₀) U) ≤ ↑(index ↑K ↑K₀)
rw [div_le_iff] <;> norm_cast
no goals
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : Set.Nonempty (interior U)
⊢ index (↑K) U ≤ index ↑K ↑K₀ * index (↑K₀) U
apply le_index_mul K₀ K hU
no goals
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : Set.Nonempty (interior U)
⊢ 0 < index (↑K₀) U
exact index_pos K₀ hU