sigma

Mathlib.Data.Multiset.Bind

URI: https://scilib.ai/kg/mathlib#Multiset.sigma

← MathLib Explorer

English

Another formulation: 0 ×ˢ t = 0.

Русский

Ещё одно формулирование: 0 ×ˢ t = 0.

LaTeX

$$$0 \times^{\mathrm{SProd}} t = 0$$$

Lean4

/-- `Multiset.sigma s t` is the dependent version of `Multiset.product`. It is the sum of
  `(a, b)` as `a` ranges over `s` and `b` ranges over `t a`. -/
protected def sigma (s : Multiset α) (t : ∀ a, Multiset (σ a)) : Multiset (Σ a, σ a) :=
  s.bind fun a => (t a).map <| Sigma.mk a

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru