English
In a monoid, an element a belongs to the product of a list of sets s: Fin n → Set α if and only if there exists a choice function f assigning to each i ∈ Fin n an element of s(i) such that the product of these chosen elements equals a.
Русский
В моноиде элемент a принадлежит произведению списка множеств s: Fin n → Set α, если и только если существует выборная функция f, которая каждому индексу i ∈ Fin n сопоставляет элемент из s(i) так, что произведение выбранных элементов равно a.
LaTeX
$$$ a \\in (List.ofFn\, s).prod \\iff \\exists f : \\forall i : \\mathrm{Fin}\\ n, s\\, i,\\ (List.ofFn\\, fun\\ i \\mapsto (f\\, i : \\alpha)).prod = a $$$
Lean4
@[to_additive]
theorem mem_prod_list_ofFn {a : α} {s : Fin n → Set α} :
a ∈ (List.ofFn s).prod ↔ ∃ f : ∀ i : Fin n, s i, (List.ofFn fun i ↦ (f i : α)).prod = a := by
induction n generalizing a with
| zero => simp_rw [List.ofFn_zero, List.prod_nil, Fin.exists_fin_zero_pi, eq_comm, Set.mem_one]
| succ n ih =>
simp_rw [List.ofFn_succ, List.prod_cons, Fin.exists_fin_succ_pi, Fin.cons_zero, Fin.cons_succ, mem_mul, @ih,
exists_exists_eq_and, SetCoe.exists, exists_prop]
