mem_prod_list_ofFn — Mathlib

English

For a function s : Fin n → Finset α, membership in (List.ofFn s).prod corresponds to the existence of a family of elements from each s i whose product equals a.

Русский

Для функции s : Fin n → Finset α принадлежность элементу в (List.ofFn s).prod эквивалентна существованию семейства элементов из каждого s i, чьи произведения равны элементу a.

LaTeX

$$$a \\in (List.ofFn\\ s).prod \\iff \\exists f : \\forall i : Fin n, s i,\\ (List.ofFn\\ fun i => (f i : α)).prod = a$$$

Lean4

@[to_additive]
theorem mem_prod_list_ofFn {a : α} {s : Fin n → Finset α} :
    a ∈ (List.ofFn s).prod ↔ ∃ f : ∀ i : Fin n, s i, (List.ofFn fun i => (f i : α)).prod = a :=
  by
  rw [← mem_coe, coe_list_prod, List.map_ofFn, Set.mem_prod_list_ofFn]
  rfl

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