English
With hV: (interior V).Nonempty, index(K,V) ≤ index(K,V0) · index(K0,V).
Русский
При Interior V непусто, индекс(K,V) ≤ индекс(K,V0) · индекс(K0,V).
LaTeX
$$$\operatorname{index}(K,V) \le \operatorname{index}(K,V_0) \cdot \operatorname{index}(K_0,V)$$$
Lean4
@[to_additive le_addIndex_mul]
theorem le_index_mul (K₀ : PositiveCompacts G) (K : Compacts G) {V : Set G} (hV : (interior V).Nonempty) :
index (K : Set G) V ≤ index (K : Set G) K₀ * index (K₀ : Set G) V := by
classical
obtain ⟨s, h1s, h2s⟩ := index_elim K.isCompact K₀.interior_nonempty
obtain ⟨t, h1t, h2t⟩ := index_elim K₀.isCompact hV
rw [← h2s, ← h2t, mul_comm]
refine le_trans ?_ Finset.card_mul_le
apply Nat.sInf_le; refine ⟨_, ?_, rfl⟩; rw [mem_setOf_eq]; refine Subset.trans h1s ?_
apply iUnion₂_subset; intro g₁ hg₁; rw [preimage_subset_iff]; intro g₂ hg₂
have := h1t hg₂
rcases this with ⟨_, ⟨g₃, rfl⟩, A, ⟨hg₃, rfl⟩, h2V⟩; rw [mem_preimage, ← mul_assoc] at h2V
exact mem_biUnion (Finset.mul_mem_mul hg₃ hg₁) h2V
