not_empty_hom

Mathlib.SetTheory.ZFC.Class

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

English

There is no universal set; the universal class does not belong to itself.

Русский

Не существует универсального множества; универсальный класс не принадлежит самому себе.

LaTeX

$$$\\text{univ} \\notin \\text{univ}$$$

Lean4

@[simp]
theorem not_empty_hom (x : ZFSet.{u}) : ¬(∅ : Class.{u}) x :=
  id

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

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

Разделы

Аффилиация

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