mem_irrefl

Mathlib.SetTheory.ZFC.Basic

URI: https://scilib.ai/kg/mathlib#ZFSet.mem_irrefl

English

For every set x, x ∉ x.

Русский

Для каждого множества x верно, что x не принадлежит самому себе.

LaTeX

$$$x \\notin x$$$

Lean4

theorem mem_irrefl (x : ZFSet) : x ∉ x :=
  irrefl_of (· ∈ ·) x

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

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

Разделы

Аффилиация

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