coe_prod — Mathlib

English

The coercion from Finset α to Set α preserves finite products: the coerced product equals the product of coerced factors.

Русский

Строгое перенесение из Finset в Set сохраняет произведения: образ произведения равен произведению образов.

LaTeX

$$$\uparrow\big(\prod i \in s, f i\big) = \prod i \in s, (f i : Set \alpha)$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_prod (s : Finset ι) (f : ι → Finset α) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, (f i : Set α) :=
  map_prod ((coeMonoidHom) : Finset α →* Set α) _ _

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