exists_cons_of_mem — Mathlib

English

If a is an element of a multiset s, then there exists a multiset t such that s is obtained by inserting a into t, i.e., s = a ::ₘ t.

Русский

Если элемент a принадлежит мультесету s, существует мультесет t, такой что s получается добавлением a в t, то есть s = a ::ₘ t.

LaTeX

$$$\\forall s:\\mathrm{Multiset}\\alpha\\,\\forall a:\\alpha,\\ a \\in s \\rightarrow \\exists t,\\ s = a ::ₘ t$$$

Lean4

theorem exists_cons_of_mem {s : Multiset α} {a : α} : a ∈ s → ∃ t, s = a ::ₘ t :=
  Quot.inductionOn s fun l (h : a ∈ l) =>
    let ⟨l₁, l₂, e⟩ := append_of_mem h
    e.symm ▸ ⟨(l₁ ++ l₂ : List α), Quot.sound perm_middle⟩

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