English
Let A be a seminormed commutative group. For natural numbers n and m with m > 0 and any real δ, the set of m-th powers of elements y that lie within δ of elements of order n·m is contained in the δ-ball around elements of order n, scaled by m. In symbols, the image under the m-th power map of approxOrderOf(A, n·m, δ) is contained in approxOrderOf(A, n, m·δ).
Русский
Пусть A — полугруппа с нормой, коммутативная. Пусть n, m ∈ ℕ, m > 0 и δ ∈ ℝ. Тогда множество степенных элементов y^m, которые лежат в пределах δ от элементов порядка n·m, находится внутри δ-окрестности элементов порядка n, при этом δ масштабируется на m: (y^m) при y ∈ approxOrderOf(A, n·m, δ) ⊆ approxOrderOf(A, n, m·δ).
LaTeX
$$$$ \\{ y^m \\;|\\; y \\in \\operatorname{approxOrderOf}(A, n m, \\delta) \\} \\subseteq \\operatorname{approxOrderOf}(A, n, m\\delta). $$$$
Lean4
@[to_additive]
theorem image_pow_subset (n : ℕ) (hm : 0 < m) :
(fun (y : A) => y ^ m) '' approxOrderOf A (n * m) δ ⊆ approxOrderOf A n (m * δ) :=
by
rintro - ⟨a, ha, rfl⟩
obtain ⟨b, hb : orderOf b = n * m, hab : a ∈ ball b δ⟩ := mem_approxOrderOf_iff.mp ha
replace hb : b ^ m ∈ {y : A | orderOf y = n} := by
rw [mem_setOf_eq, orderOf_pow' b hm.ne', hb, Nat.gcd_mul_left_left, n.mul_div_cancel hm]
apply ball_subset_thickening hb (m * δ)
convert pow_mem_ball hm hab using 1
simp only [nsmul_eq_mul]
