subtypePerm_apply_pow_of_mem — Mathlib

English

Let g be a permutation of α and s a finite set such that g preserves s (g(x) ∈ s iff x ∈ s). For any n, the n-th power of the restricted permutation on s, evaluated at ⟨x, hx⟩, equals g^n(x) for any x ∈ s.

Русский

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

LaTeX

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

Lean4

theorem subtypePerm_apply_pow_of_mem {g : Perm α} {s : Finset α} (hs : ∀ x : α, g x ∈ s ↔ x ∈ s) {n : ℕ} {x : α}
    (hx : x ∈ s) : ((g.subtypePerm hs ^ n) (⟨x, hx⟩ : s) : α) = (g ^ n) x := by
  simp only [subtypePerm_pow, subtypePerm_apply]

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