singleton_le — Mathlib

English

The singleton {a} is a submultiset of s iff a ∈ s.

Русский

Мультимножество {a} подпадает под s тогда и только тогда, когда a принадлежит s.

LaTeX

$${a} \le s \\iff a \in s$$

Lean4

@[simp]
theorem singleton_le {a : α} {s : Multiset α} : { a } ≤ s ↔ a ∈ s :=
  ⟨fun h => mem_of_le h (mem_singleton_self _), fun h =>
    let ⟨_t, e⟩ := exists_cons_of_mem h
    e.symm ▸ cons_le_cons _ (zero_le _)⟩

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