cons_inj_right

Mathlib.Data.Multiset.ZeroCons

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

English

For any a, s,t, a ::ₘ s = a ::ₘ t iff s = t.

Русский

Для любых a, s, t, a ::ₘ s = a ::ₘ t эквивалентно s = t.

LaTeX

$$a ::ₘ s = a ::ₘ t \\iff s = t$$

Lean4

@[simp]
theorem cons_inj_right (a : α) : ∀ {s t : Multiset α}, a ::ₘ s = a ::ₘ t ↔ s = t := by rintro ⟨l₁⟩ ⟨l₂⟩; simp

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

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

Разделы

Аффилиация

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