cons_sigma — Mathlib

English

The sigma operation distributes over cons in the general form: (a ::ₘ s).sigma t = (t a).map (Sigma.mk a) + s.sigma t.

Русский

Описывается обобщённое распределение сигмы на cons: (a ::ₘ s).sigma t = (t a).map (Sigma.mk a) + s.sigma t.

LaTeX

$$$(a ::ₘ s).\sigma t = (t a).map(\Sigma.mk a) + s.\sigma t$$$

Lean4

@[simp]
theorem cons_sigma : (a ::ₘ s).sigma t = (t a).map (Sigma.mk a) + s.sigma t := by simp [Multiset.sigma]

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