English
Let G be a group and H a subgroup. Then G is finite if and only if H is finite and the index [G : H] is finite.
Русский
Пусть G — группа, H — подгруппа. Тогда G конечно по мощности тогда и только тогда, когда H конечно и индекс [G : H] конечно.
LaTeX
$$$|G| < \infty \;\Longrightarrow\; (|H| < \infty \;\land\; [G:H] < \infty) \\ (|H| < \infty \land [G:H] < \infty) \Rightarrow |G| < \infty$$$
Lean4
@[to_additive]
theorem finite_iff_finite_and_finiteIndex : Finite G ↔ Finite H ∧ H.FiniteIndex
where
mp _ := ⟨inferInstance, inferInstance⟩
mpr := fun ⟨_, _⟩ ↦
Nat.finite_of_card_ne_zero <| H.card_mul_index ▸ mul_ne_zero Nat.card_pos.ne' FiniteIndex.index_ne_zero