list_prod_singleton — Mathlib

English

The product of singleton sets formed from a function I is the singleton of the product of I's values.

Русский

Произведение одиночных множеств ${I(i)}$ равно одиночному множеству, содержащему произведение всех I(i).

LaTeX

$$(t.map fun i => ({ I i } : Set M)).prod = { t.prod fun i => I i }$$

Lean4

@[to_additive]
theorem list_prod_singleton {M : Type*} [Monoid M] (s : List M) : (s.map fun i ↦ ({ i } : Set M)).prod = { s.prod } :=
  (map_list_prod (singletonMonoidHom : M →* Set M) _).symm

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