index_elim — Mathlib

English

There exists a finite t such that K is covered by left translates of V and the card of t equals the Haar index.

Русский

Существует конечное множество t такое, что K покрывается левыми сдвигами V и карточка t равна Haar индексу.

LaTeX

$$$\\exists t: Finset\,G, (K \\subseteq \\bigcup_{g \\in t} (g \\cdot -)^{-1}' V) \\land \\operatorname{card}(t) = \\operatorname{index}(K,V)$$$

Lean4

@[to_additive addIndex_elim]
theorem index_elim {K V : Set G} (hK : IsCompact K) (hV : (interior V).Nonempty) :
    ∃ t : Finset G, (K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V) ∧ Finset.card t = index K V := by
  have := Nat.sInf_mem (index_defined hK hV); rwa [mem_image] at this

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