mem_irrefl

Mathlib.SetTheory.ZFC.PSet

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

English

No pre-set contains itself.

Русский

Никакое предмножество не содержит само себя.

LaTeX

$$$\\forall x:\\mathrm{PSet},\\ x\\notin x$$$

Lean4

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

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

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

Разделы

Аффилиация

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