exists_multiset_cons — Mathlib

English

If s is covered by t in the multiset order, then t is obtained from s by adding a single new element at the front: t = a ::ₘ s for some a.

Русский

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

LaTeX

$$$ (\exists a)\ (a ::ₘ s) = t $$$

Lean4

theorem _root_.CovBy.exists_multiset_cons (h : s ⋖ t) : ∃ a, a ::ₘ s = t :=
  (lt_iff_cons_le.1 h.lt).imp fun _a ha ↦ ha.eq_of_not_lt <| h.2 <| lt_cons_self _ _

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