card_pos

Mathlib.Data.Multiset.ZeroCons

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

English

A multiset has positive cardinality if and only if it is nonempty.

Русский

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

LaTeX

$$0 < card(s) \iff s \neq 0$$

Lean4

theorem card_pos {s : Multiset α} : 0 < card s ↔ s ≠ 0 :=
  Nat.pos_iff_ne_zero.trans <| not_congr card_eq_zero

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

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

Разделы

Аффилиация

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