uniqueEmpty

Mathlib.Data.Set.Basic

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

← MathLib Explorer

English

There is exactly one empty set on a type when IsEmpty holds.

Русский

Существует ровно одно пустое множество на данную вершину типа, если выполнено IsEmpty.

LaTeX

$$$$ \exists! X \subseteq \alpha, X = \emptyset. $$$$

Lean4

/-- There is exactly one set of a type that is empty. -/
instance uniqueEmpty [IsEmpty α] : Unique (Set α) where
  default := ∅
  uniq := eq_empty_of_isEmpty

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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