cons_inj_left — Mathlib

English

For any s, a ::ₘ s = b ::ₘ s implies a = b.

Русский

Для произвольного s, a ::ₘ s = b ::ₘ s тогда и только тогда a = b.

LaTeX

$${a} ::ₘ {s} = {b} ::ₘ {s} \\iff a = b$$

Lean4

@[simp]
theorem cons_inj_left {a b : α} (s : Multiset α) : a ::ₘ s = b ::ₘ s ↔ a = b :=
  ⟨Quot.inductionOn s fun l e =>
      have : [a] ++ l ~ [b] ++ l := Quotient.exact e
      singleton_perm_singleton.1 <| (perm_append_right_iff _).1 this,
    congr_arg (· ::ₘ _)⟩

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