coe_eq_singleton — Mathlib

English

A list coerced to a multiset equals the singleton of an element a if and only if the list is exactly [a].

Русский

Список, приводимый к мультимножеству, равен одиночному мультимножеству {a} тогда и только тогда, когда список равен [a].

LaTeX

$$$(l : \\mathrm{Multiset}\\alpha) = {a} \\iff l = [a]$$$

Lean4

@[simp, norm_cast]
theorem coe_eq_singleton {l : List α} {a : α} : (l : Multiset α) = { a } ↔ l = [a] := by
  rw [← coe_singleton, coe_eq_coe, List.perm_singleton]

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