card

Mathlib.Data.Finset.Card

URI: https://scilib.ai/kg/mathlib#Finset.card

← MathLib Explorer

English

For any Finset s, we have #s ≠ 0 if and only if s is nonempty.

Русский

Для любого финсета s имеем #s ≠ 0 тогда и только тогда, когда s непуст.

LaTeX

$$$#s \neq 0 \iff s \neq \emptyset$$$

Lean4

/-- `s.card` is the number of elements of `s`, aka its cardinality.

The notation `#s` can be accessed in the `Finset` locale. -/
def card (s : Finset α) : ℕ :=
  Multiset.card s.1

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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