zpow_disjoint_zpow — Mathlib

English

If σ and τ are disjoint, then for any integers m, n, the permutations σ^m and τ^n are disjoint.

Русский

Если σ и τ разнесены, то для любых целых чисел m, n перестановки σ^m и τ^n разнесены.

LaTeX

$$$$ \forall \sigma, \tau\ (\operatorname{Disjoint}(\sigma,\tau)\Rightarrow \forall m,n\in \mathbb{Z},\ \operatorname{Disjoint}(\sigma^m,\tau^n)). $$$$

Lean4

theorem zpow_disjoint_zpow {σ τ : Perm α} (hστ : Disjoint σ τ) (m n : ℤ) : Disjoint (σ ^ m) (τ ^ n) := fun x =>
  Or.imp (fun h => zpow_apply_eq_self_of_apply_eq_self h m) (fun h => zpow_apply_eq_self_of_apply_eq_self h n) (hστ x)

Похожие утверждения