English
If X generates an infinite group and contains the identity, then the size of X^n grows at least linearly; more precisely, |X^n| ≥ n + 1 for all n.
Русский
Если X порождает бесконечную группу и содержит единицу, то размер X^n растёт не менее линейно: |X^n| ≥ n + 1 для всех n.
LaTeX
$$$|X^n| \ge n+1 \quad \text{for all } n \in \mathbb{N}$ given $1\in X$ and closure(X) infinite$$
Lean4
/-- The growth of a set generating an infinite group is at least linear. -/
@[to_additive /-- The growth of a set generating an infinite group is at least linear. -/
]
theorem add_one_le_card_pow (hX₁ : 1 ∈ X) (hXclosure : (closure (X : Set G) : Set G).Infinite) : ∀ n, n + 1 ≤ #(X ^ n)
| 0 => by simp
| n + 1 =>
(add_one_le_card_pow hX₁ hXclosure _).trans_lt <|
card_lt_card <| pow_right_strictMono hX₁ (by simp [hXclosure]) n.lt_succ_self
