card_pos_iff_exists_mem

Mathlib.Data.Multiset.ZeroCons

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

English

There exists an element of s if and only if 0 < card s.

Русский

Существует элемент множества s тогда и только тогда, когда кардинал s положителен.

LaTeX

$$0 < card(s) \iff \exists a, a \in s$$

Lean4

theorem card_pos_iff_exists_mem {s : Multiset α} : 0 < card s ↔ ∃ a, a ∈ s :=
  Quot.inductionOn s fun _l => length_pos_iff_exists_mem

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

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

Разделы

Аффилиация

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