English
Translating K by a fixed group element g only decreases the index with respect to V: index(gK, V) ≤ index(K, V).
Русский
Сдвиг левой частью на элемент g недовляет индекс: index(gK, V) ≤ index(K, V).
LaTeX
$$$\text{index}(gK, V) \le \text{index}(K, V)\quad( g \in G,\, V\text{ open},\, (\operatorname{int}V).\neq \emptyset)$$$
Lean4
@[to_additive add_left_addIndex_le]
theorem mul_left_index_le {K : Set G} (hK : IsCompact K) {V : Set G} (hV : (interior V).Nonempty) (g : G) :
index ((fun h => g * h) '' K) V ≤ index K V :=
by
rcases index_elim hK hV with ⟨s, h1s, h2s⟩; rw [← h2s]
apply Nat.sInf_le; rw [mem_image]
refine ⟨s.map (Equiv.mulRight g⁻¹).toEmbedding, ?_, Finset.card_map _⟩
simp only [mem_setOf_eq]; refine Subset.trans (image_mono h1s) ?_
rintro _ ⟨g₁, ⟨_, ⟨g₂, rfl⟩, ⟨_, ⟨hg₂, rfl⟩, hg₁⟩⟩, rfl⟩
simp only [mem_preimage] at hg₁
simp only [exists_prop, mem_iUnion, Finset.mem_map, Equiv.coe_mulRight, exists_exists_and_eq_and, mem_preimage,
Equiv.toEmbedding_apply]
refine ⟨_, hg₂, ?_⟩; simp only [mul_assoc, hg₁, inv_mul_cancel_left]
