mem_pow — Mathlib

English

For a Finset s and a, n, membership a ∈ s^n holds iff there exists a function f from Fin n to s such that the product of the chosen elements equals a.

Русский

Для конечного множества s и элемента a и натурального n, a ∈ s^n эквивалентно существованию отображения f: Fin n → s, чье произведение выбранных элементов равно a.

LaTeX

$$$a \\in s^n \\iff \\exists f : Fin n → s, \\ \\mathrm{List.ofFn} fun i => (f i).val.prod = a$$$

Lean4

@[to_additive]
theorem mem_pow {a : α} {n : ℕ} : a ∈ s ^ n ↔ ∃ f : Fin n → s, (List.ofFn fun i => ↑(f i)).prod = a := by
  simp [← mem_coe, coe_pow, Set.mem_pow]

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