notMem_empty

Mathlib.SetTheory.ZFC.Class

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

English

No element x belongs to the empty class; the empty class contains nothing.

Русский

Ни один элемент не принадлежит пустому классy; пустой класс ничего не содержит.

LaTeX

$$$\\forall x : \\text{Class}, x \\notin (\\emptyset : \\text{Class})$$$

Lean4

@[simp]
theorem notMem_empty (x : Class.{u}) : x ∉ (∅ : Class.{u}) := fun ⟨_, _, h⟩ => h

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

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

Разделы

Аффилиация

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