G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
hV : Set.Nonempty (interior V)
this :
  sInf (Finset.card '' {t | K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}) ∈
    Finset.card '' {t | K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
⊢ ∃ t, (K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V) ∧ Finset.card t = index K V
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
hV : Set.Nonempty (interior V)
⊢ ∃ t, (K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V) ∧ Finset.card t = index K V
have := Nat.sInf_mem (index_defined hK hV)
no goals
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
hV : Set.Nonempty (interior V)
this :
  sInf (Finset.card '' {t | K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}) ∈
    Finset.card '' {t | K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
⊢ ∃ t, (K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V) ∧ Finset.card t = index K V
rwa [mem_image] at this