countable_empty

Mathlib.Data.Set.Countable

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

English

The empty set is countable.

Русский

Пустое множество счетно.

LaTeX

$$$(\\emptyset:\\ Set\\,\\alpha).Countable$$$

Lean4

@[simp]
theorem countable_empty : (∅ : Set α).Countable :=
  to_countable _

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

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

Разделы

Аффилиация

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