coe_pow — Mathlib

English

For any Finset s and natural number n, the underlying set of s^n equals the nth power of the underlying set: ↑(s^n) = (↑s)^n.

Русский

Для любого конечного множества s и натурального числа n основное множество s^n совпадает с n-й степенью множества s, взятого как множество: ↑(s^n) = (s)^n.

LaTeX

$$$\\uparrow (s^n) = (s : Set \\alpha)^n$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_pow (s : Finset α) (n : ℕ) : ↑(s ^ n) = (s : Set α) ^ n :=
  by
  change ↑(npowRec n s) = (s : Set α) ^ n
  induction n with
  | zero => rw [npowRec, pow_zero, coe_one]
  | succ n ih => rw [npowRec, pow_succ, coe_mul, ih]

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