perm_zpow — Mathlib

English

For any integer power, a bijection on s remains a bijection when raised to the integral power, i.e., f^n is bijective on s for all integers n.

Русский

Для любого целого показателя f^n остаётся биекцией на s для всех целых n.

LaTeX

$$∀ n ∈ ℤ, BijOn (f ^ n) s s$$

Lean4

theorem perm_zpow (hf : BijOn f s s) : ∀ n : ℤ, BijOn (f ^ n) s s
  | Int.ofNat n => hf.perm_pow n
  | Int.negSucc n => (hf.perm_pow (n + 1)).perm_inv

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