is_left_invariant_index — Mathlib

English

For every left translation by g, the index is preserved: index(gK, V) = index(K, V).

Русский

При любом левом переносе на g индекс сохраняется: index(gK, V) = index(K, V).

LaTeX

$$$\text{index}(gK, V) = \text{index}(K, V)$$$

Lean4

@[to_additive is_left_invariant_addIndex]
theorem is_left_invariant_index {K : Set G} (hK : IsCompact K) (g : G) {V : Set G} (hV : (interior V).Nonempty) :
    index ((fun h => g * h) '' K) V = index K V :=
  by
  refine le_antisymm (mul_left_index_le hK hV g) ?_
  convert mul_left_index_le (hK.image <| continuous_mul_left g) hV g⁻¹
  rw [image_image]; symm; convert image_id' _ with h; apply inv_mul_cancel_left

Похожие утверждения