coe_list_prod — Mathlib

English

For a list s of Finset α, the underlying set of the product of s equals the product (in Set) of the underlying sets: (↑s.prod) = ∏ (↑s_i).

Русский

Для списка s Finset α множество произведения равняется произведению множеств: (↑s.prod) = ∏ (↑s_i).

LaTeX

$$$\\uparrow (s.prod) = \\left( \\prod_i (s_i)^{\\uparrow} \\right)$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_list_prod (s : List (Finset α)) : (↑s.prod : Set α) = (s.map (↑)).prod :=
  map_list_prod (coeMonoidHom : Finset α →* Set α) _

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