English
If the translates of K1 and K2 by V^{-1} are disjoint, then the index of their union equals the sum of the individual indices: index(K1 ∪ K2, V) = index(K1, V) + index(K2, V).
Русский
Если K1·V^{-1} и K2·V^{-1} раздельны, то index(K1 ∪ K2, V) = index(K1, V) + index(K2, V).
LaTeX
$$$\text{index}(K_1 \cup K_2, V) = \text{index}(K_1, V) + \text{index}(K_2, V) \quad\text{при }(K_1 V^{-1}) \cap (K_2 V^{-1}) = \emptyset$$$
Lean4
@[to_additive addIndex_union_eq]
theorem index_union_eq (K₁ K₂ : Compacts G) {V : Set G} (hV : (interior V).Nonempty)
(h : Disjoint (K₁.1 * V⁻¹) (K₂.1 * V⁻¹)) : index (K₁.1 ∪ K₂.1) V = index K₁.1 V + index K₂.1 V := by
classical
apply le_antisymm (index_union_le K₁ K₂ hV)
rcases index_elim (K₁.2.union K₂.2) hV with ⟨s, h1s, h2s⟩; rw [← h2s]
have (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (g * ·) ⁻¹' V) : index K V ≤ {g ∈ s | ((g * ·) ⁻¹' V ∩ K).Nonempty}.card :=
by
apply Nat.sInf_le; refine ⟨_, ?_, rfl⟩; rw [mem_setOf_eq]
intro g hg; rcases hK hg with ⟨_, ⟨g₀, rfl⟩, _, ⟨h1g₀, rfl⟩, h2g₀⟩
simp only [mem_preimage] at h2g₀
simp only [mem_iUnion]; use g₀; constructor; swap
· simp only [Finset.mem_filter, h1g₀, true_and]; use g
simp [hg, h2g₀]
exact h2g₀
refine
le_trans
(add_le_add (this K₁.1 <| Subset.trans subset_union_left h1s) (this K₂.1 <| Subset.trans subset_union_right h1s))
?_
rw [← Finset.card_union_of_disjoint, Finset.filter_union_right]
· exact s.card_filter_le _
apply Finset.disjoint_filter.mpr
rintro g₁ _ ⟨g₂, h1g₂, h2g₂⟩ ⟨g₃, h1g₃, h2g₃⟩
simp only [mem_preimage] at h1g₃ h1g₂
refine h.le_bot (?_ : g₁⁻¹ ∈ _)
constructor <;> simp only [Set.mem_inv, Set.mem_mul]
· refine ⟨_, h2g₂, (g₁ * g₂)⁻¹, ?_, ?_⟩
· simp only [inv_inv, h1g₂]
· simp only [mul_inv_rev, mul_inv_cancel_left]
· refine ⟨_, h2g₃, (g₁ * g₃)⁻¹, ?_, ?_⟩
· simp only [inv_inv, h1g₃]
· simp only [mul_inv_rev, mul_inv_cancel_left]
