English
Let G be a topological group with continuous multiplication and inversion. If x specializes to y (x ⤳ y), then for every integer m, x^m specializes to y^m.
Русский
Пусть G — топологическая группа с непрерывной операцией умножения и обращением. Если x эквивалентно y по отношению специализации (x ⤳ y), тогда для каждого целого m выполняется x^m ⤳ y^m.
LaTeX
$$$\\\\forall G\\ [\\\\operatorname{DivInvMonoid} G] [\\\\operatorname{TopologicalSpace} G] [\\\\operatorname{ContinuousMul} G] [\\\\operatorname{ContinuousInv} G], \\\\forall x,y \\in G, x \\\\curvearrowright y \\\\Rightarrow \\\\forall m \\\\in \\\\mathbb{Z}, x^m \\\\curvearrowright y^m.$$$
Lean4
@[to_additive]
protected theorem zpow {G : Type*} [DivInvMonoid G] [TopologicalSpace G] [ContinuousMul G] [ContinuousInv G] {x y : G}
(h : x ⤳ y) : ∀ m : ℤ, (x ^ m) ⤳ (y ^ m)
| .ofNat n => by simpa using h.pow n
| .negSucc n => by simpa using (h.pow (n + 1)).inv
