English
If x and y are inseparable in a topological group, then for every integer m, x^m and y^m are inseparable.
Русский
Если 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, \\\\operatorname{Inseparable} x y \\\\Rightarrow \\\\forall m \\\\in \\\\mathbb{Z}, \\\\operatorname{Inseparable} (x^m) (y^m).$$$
Lean4
@[to_additive]
protected theorem zpow {G : Type*} [DivInvMonoid G] [TopologicalSpace G] [ContinuousMul G] [ContinuousInv G] {x y : G}
(h : Inseparable x y) (m : ℤ) : Inseparable (x ^ m) (y ^ m) :=
(h.specializes.zpow m).antisymm (h.specializes'.zpow m)
