mem_pow_iff_prod — Mathlib

English

Membership in the nth power of a set corresponds to a product of n elements chosen from the set.

Русский

Принадлежность к s^n означает существование n элементов из s, их произведение равно данному элементу.

LaTeX

$$a ∈ s^n ↔ ∃ f : Fin n → α, ∀ i, f i ∈ s ∧ ∏ i, f i = a$$

Lean4

@[to_additive]
theorem mem_pow_iff_prod {n : ℕ} {s : Set α} {a : α} : a ∈ s ^ n ↔ ∃ f : Fin n → α, (∀ i, f i ∈ s) ∧ ∏ i, f i = a := by
  simpa using mem_finset_prod (t := .univ) (f := fun _ : Fin n ↦ s) _

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