ncard

Mathlib.Data.Set.Card

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

English

The ncard of s is defined as ENat.toNat of encard s; it gives 0 for infinite encards.

Русский

ncard множества s определяется как ENat.toNat(encard s); для бесконечной encard значение равно 0.

LaTeX

$$$ s.ncard = ENat.toNat s.encard $$$

Lean4

/-- The cardinality of `s : Set α` . Has the junk value `0` if `s` is infinite -/
noncomputable def ncard (s : Set α) : ℕ :=
  ENat.toNat s.encard

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

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

Разделы

Аффилиация

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