image_op_pow — Mathlib

English

For any Finset s, and any natural n, applying the op map to s^n yields the n-th power of the image of s under op: image(op)(s^n) = image(op)(s)^n.

Русский

Для любого Finset s и любого n выполняется: image(op)(s^n) = image(op)(s)^n.

LaTeX

$$$(\mathrm{image}\,\mathrm{op})(s^n) = (\mathrm{image}\,\mathrm{op})(s)^n$$$

Lean4

@[to_additive]
theorem image_op_pow (s : Finset α) : ∀ n : ℕ, (s ^ n).image op = s.image op ^ n
  | 0 => by simp [singleton_one]
  | n + 1 => by rw [pow_succ, pow_succ', image_op_mul, image_op_pow]

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