coe_subsingletonEquiv — Mathlib

English

If α is a subsingleton, the standard equivalence from lists to multisets coincides with the canonical singleton-to-multiset mapping.

Русский

Если α является подсинглетоном, то стандартное отображение списков в мультимножества совпадает с каноническим отображением одиночного элемента в мультимножество.

LaTeX

$$$ [\\text{Subsingleton }\\alpha] : (\\text{List }\\alpha \\to Multiset\\alpha) = \\operatorname{ofList}$$$

Lean4

@[simp]
theorem coe_subsingletonEquiv [Subsingleton α] : (subsingletonEquiv α : List α → Multiset α) = ofList :=
  rfl

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