empty_or_exists_mem

Mathlib.Data.Multiset.ZeroCons

URI: https://scilib.ai/kg/mathlib#Multiset.empty_or_exists_mem

English

Every multiset is either empty or contains some element.

Русский

Каждое мультимножество либо пусто, либо содержит некоторый элемент.

LaTeX

$$$s = 0 \\lor \\exists a:\\alpha, a \\in s$$$

Lean4

theorem empty_or_exists_mem (s : Multiset α) : s = 0 ∨ ∃ a, a ∈ s :=
  or_iff_not_imp_left.mpr Multiset.exists_mem_of_ne_zero

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru