English
Let l be a list of sets in a monoid. An element a lies in the product l.prod if and only if there exists a list l' consisting of pairs (S, x) with x ∈ S and the first components of these pairs form l, and the product of the second components equals a.
Русский
Пусть l — список множеств в моноиде. Элемент a принадлежит произведению l.prod тогда и только тогда, когда существует список l', состоящий из пар (S, x) с x ∈ S, где первые компоненты пар образуют l, а произведение вторых компонентов равно a.
LaTeX
$$$ a \\in l.prod \\iff \\exists l' : List (\\Sigma s : Set \\alpha, \\ ↥s),\\; List.prod (l'.map fun x \\mapsto (Sigma.snd x : \\alpha)) = a \\land\\; l'.map Sigma.fst = l $$$
Lean4
@[to_additive]
theorem mem_list_prod {l : List (Set α)} {a : α} :
a ∈ l.prod ↔
∃ l' : List (Σ s : Set α, ↥s), List.prod (l'.map fun x ↦ (Sigma.snd x : α)) = a ∧ l'.map Sigma.fst = l :=
by
induction l using List.ofFnRec with
| _ n f
simp only [mem_prod_list_ofFn, List.exists_iff_exists_tuple, List.map_ofFn, List.ofFn_inj', Sigma.mk.inj_iff,
and_left_comm, exists_and_left, exists_eq_left, heq_eq_eq]
constructor
· rintro ⟨fi, rfl⟩
exact ⟨fun i ↦ ⟨_, fi i⟩, rfl, rfl⟩
· rintro ⟨fi, rfl, rfl⟩
exact ⟨fun i ↦ _, rfl⟩
