mem_irrefl

Mathlib.SetTheory.ZFC.Class

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

English

No object is a member of itself: x ∉ x for all x in Class.

Русский

Ни один объект не является элементом самого себя: x ∉ x для всех x в Class.

LaTeX

$$$\\\\forall x : Class, \\\\neg (\\\\mathrm{instMembership}.mem x x).$$$

Lean4

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

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

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

Разделы

Аффилиация

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