fst_prod — Mathlib

English

Let s be a finite multiset of ordered pairs (x, y) with x in M and y in N. Then the first component of the product over s equals the product of the first components.

Русский

Пусть s — конечная мультипетя пар (x, y) с x в M и y в N. Тогда первая координата произведения по s равна произведению первых координат.

LaTeX

$$$\\left( \\prod s \\right)_1 = \\left( \\prod (s.map \\mathrm{fst}) \\right)$$$

Lean4

@[to_additive]
theorem fst_prod (s : Multiset (M × N)) : s.prod.1 = (s.map Prod.fst).prod :=
  map_multiset_prod (MonoidHom.fst _ _) _

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