singleton_eq_cons_iff

Mathlib.Data.Multiset.ZeroCons

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

← MathLib Explorer

English

The singleton {a} equals b :: m if and only if a = b and m = 0.

Русский

Единичный мультимножество {a} равно b :: m тогда и только тогда, когда a = b и m = 0.

LaTeX

$$$\\{a\\} = b ::ₘ m \\iff a = b \\land m = 0$$$

Lean4

@[simp]
theorem singleton_eq_cons_iff {a b : α} (m : Multiset α) : { a } = b ::ₘ m ↔ a = b ∧ m = 0 :=
  by
  rw [← cons_zero, cons_eq_cons]
  simp [eq_comm]

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

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

Разделы

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

Аффилиация

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