subtypePerm_apply_zpow_of_mem — Mathlib

English

Let g be a permutation of α and s a finite set invariant under g. For every integer exponent i, the i-th power of the restricted permutation on s, evaluated at ⟨x, hx⟩, equals g^i(x).

Русский

Пусть g — перестановка α и s — множество, инвариантное относительно g. Для любого целого i степенная ограниченная перестановка по s удовлетворяет (g_subtype hs)^i(⟨x,hx⟩) = g^i x.

LaTeX

$$$\\big( g_{|s} \\big)^i (\\langle x, hx \\rangle) = g^i x$$$

Lean4

theorem subtypePerm_apply_zpow_of_mem {g : Perm α} {s : Finset α} (hs : ∀ x : α, g x ∈ s ↔ x ∈ s) {i : ℤ} {x : α}
    (hx : x ∈ s) : ((g.subtypePerm hs ^ i) (⟨x, hx⟩ : s) : α) = (g ^ i) x := by
  simp only [subtypePerm_zpow, subtypePerm_apply]

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