empty

Mathlib.Logic.Equiv.Set

URI: https://scilib.ai/kg/mathlib#Equiv.Set.empty

English

There is a canonical bijection between the empty set ∅ and the Empty type.

Русский

Существует каноническая биекция между пустым множеством и типом Empty.

LaTeX

$$$(\emptyset : \mathrm{Set}\,\alpha) \cong Empty$$$

Lean4

/-- An empty set is equivalent to the `Empty` type. -/
protected def empty (α) : (∅ : Set α) ≃ Empty :=
  equivEmpty _

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

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

Разделы

Аффилиация

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