zero_ne_cons — Mathlib

English

The empty multiset is different from any nonempty cons multiset.

Русский

Пустое мультимножество не равно некому конструированному через cons.

LaTeX

$$$\\forall a:\\alpha,\\forall m:\\mathrm{Multiset}\\alpha,\\ 0 \\neq a ::ₘ m$$$

Lean4

@[simp]
theorem zero_ne_cons {a : α} {m : Multiset α} : 0 ≠ a ::ₘ m := fun h =>
  have : a ∈ (0 : Multiset α) := h.symm ▸ mem_cons_self _ _
  notMem_zero _ this

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