English
If X is a finite subset of a group with 1 ∈ X and X nontrivial, then the map n ↦ X^n is strictly monotone on the indices where (X^{n-1}) is not equal to the closure of X.
Русский
Если X — конечное подмножество группы с 1 в X и X не тривиально, то отображение n ↦ X^n строго монотонно на множествах индексов, где X^{n-1} не равно замыканию X.
LaTeX
$$$\forall G \; \forall X \subseteq G,\; 1\in X,\; X \text{ Nontrivial} \Rightarrow\; \text{StrictMonoOn}(\lambda n, X^n, \{n \mid (X^{n-1}) \neq \overline{X}\})$$$
Lean4
@[to_additive]
theorem pow_right_strictMonoOn (hX₁ : 1 ∈ X) (hX : X.Nontrivial) :
StrictMonoOn (fun n ↦ X ^ n) {n | (X ^ (n - 1) : Set G) ≠ closure (X : Set G)} :=
by
refine strictMonoOn_of_lt_add_one ⟨?_⟩ fun n _ _ hn ↦ pow_ssubset_pow_succ_of_pow_ne_closure hX₁ hX hn
rintro - - n hn m ⟨-, hmn⟩ hm
apply hn
obtain rfl | hm₀ := m.eq_zero_or_pos
· simp [eq_comm (a := (1 : Set _)), coe_set_eq_one, -Set.subset_singleton_iff, hX.coe.not_subset_singleton] at hm
·
calc
(X : Set G) ^ (n - 1)
_ = X ^ (n - m) * X ^ (m - 1) := by rw [← pow_add]; congr 1; cutsat
_ = closure (X : Set G) := by rw [hm, Set.pow_mul_subgroupClosure hX.nonempty.to_set]
