coe_sigma — Mathlib

English

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

Русский

Операция сигма распространяется на конc: (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 coe_sigma (l₁ : List α) (l₂ : ∀ a, List (σ a)) : (@Multiset.sigma α σ l₁ fun a => l₂ a) = l₁.sigma l₂ :=
  by
  rw [Multiset.sigma, List.sigma, ← coe_bind]
  simp

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