encard

Mathlib.Data.Set.Card

URI: https://scilib.ai/kg/mathlib#Set.encard

English

The encard of a set is the ENat-valued cardinality of that set.

Русский

encard множества есть ENat-количество элементов этого множества.

LaTeX

$$$ \operatorname{encard}(s) = \operatorname{ENat.card}(s) $$$

Lean4

/-- The cardinality of a set as a term in `ℕ∞` -/
noncomputable def encard (s : Set α) : ℕ∞ :=
  ENat.card s

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

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

Разделы

Аффилиация

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