univ_notMem_univ

Mathlib.SetTheory.ZFC.Class

URI: https://scilib.ai/kg/mathlib#Class.univ_notMem_univ

← MathLib Explorer

English

There is no universal set: univ ∉ univ.

Русский

Нет универсального множества: univ ∉ univ.

LaTeX

$$$ univ \\notin univ $$$

Lean4

/-- **There is no universal set.**
This is stated as `univ ∉ univ`, meaning that `univ` (the class of all sets) is proper (does not
belong to the class of all sets). -/
theorem univ_notMem_univ : univ ∉ univ :=
  mem_irrefl _

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

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

Разделы

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

Аффилиация

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