English
In a group, if 1 is in X and X is nontrivial, and the nth power set of X is not contained in the subgroup closure of X, then X^n is strictly contained in X^{n+1}. In other words, the powers of X strictly grow past n.
Русский
В группе множество X содержит единицу и не тривиально; если X^n не включено в замыкание подгруппы, порождённой X, то X^n ⊊ X^{n+1}. Иными словами, степени множества растут строго после n.
LaTeX
$$$\forall G \text{ group},\; \forall X \subseteq G \text{ Finset},\; 1 \in X,\; X \text{ Nontrivial},\; X^n \n\subseteq \mathrm{closure}(X)\Rightarrow X^n \subsetneq X^{n+1}$$$
Lean4
@[to_additive]
theorem pow_ssubset_pow_succ_of_pow_ne_closure (hX₁ : (1 : G) ∈ X) (hX : X.Nontrivial)
(hXclosure : (X ^ n : Set G) ≠ closure (X : Set G)) : X ^ n ⊂ X ^ (n + 1) :=
by
obtain rfl | hn := eq_or_ne n 0
· simpa [ssubset_iff_subset_not_subset, hX₁, -Finset.subset_singleton_iff] using hX.not_subset_singleton
refine (pow_subset_pow_right hX₁ <| n.le_add_right _).ssubset_of_ne ?_
contrapose! hXclosure with hXn
rw [← closure_pow (mod_cast hX₁) hn]
wlog hn₁ : n = 1
· simp +contextual only [pow_one] at this
replace hXn d : X ^ (n + d) = X ^ n := by
induction d with
| zero => rw [add_zero]
| succ d hd =>
rw [pow_add, pow_one] at hXn
rw [← add_assoc, pow_add, pow_one, hd, ← hXn]
exact mod_cast this (one_mem_pow hX₁) (hX.pow hn) one_ne_zero (by simp [hXn, ← pow_mul, mul_two]) (by simp)
subst hn₁
simp only [ne_eq, one_ne_zero, not_false_eq_true, Nat.reduceAdd, pow_one] at *
let Xgp : Subgroup G :=
{ carrier := X
mul_mem' := fun {x y} hx hy ↦ by
norm_cast at *
simpa [← hXn, ← sq] using mul_mem_mul hx hy
one_mem' := hX₁
inv_mem' := fun {x} hx ↦ by
norm_cast at *
have : x • X ⊆ X := by simpa [← hXn, add_assoc, ← sq] using smul_finset_subset_mul (t := X) hx
have : x • X = X := eq_of_subset_of_card_le this (card_smul_finset ..).ge
rw [← eq_inv_smul_iff] at this
rw [this]
simpa [mem_inv_smul_finset_iff] }
exact subset_closure.antisymm <| (closure_le Xgp).2 subset_rfl
