mk_emptyCollection

Mathlib.SetTheory.Cardinal.Basic

URI: https://scilib.ai/kg/mathlib#Cardinal.mk_emptyCollection

English

The empty set has cardinality zero.

Русский

Пустое множество имеет кардинальность равную нулю.

LaTeX

$$$|\\emptyset| = 0$$$

Lean4

theorem mk_emptyCollection (α : Type u) : #(∅ : Set α) = 0 :=
  mk_eq_zero _

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

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

Разделы

Аффилиация

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