product_singleton — Mathlib

English

The product of a singleton a and a singleton b yields the singleton {(a,b)}.

Русский

Произведение одиночного элемента a и одиночного элемента b даёт единственный элемент пары {(a,b)}.

LaTeX

$$$({ a } : \mathrm{Multiset}\ \alpha) \times^{\mathrm{SProd}} ({ b } : \mathrm{Multiset}\ \beta) = \{(a,b)\}$$$

Lean4

@[simp]
theorem product_singleton : ({ a } : Multiset α) ×ˢ ({ b } : Multiset β) = {(a, b)} := by
  simp only [SProd.sprod, product, bind_singleton, map_singleton]

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