mem_asymm

Mathlib.SetTheory.ZFC.Class

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

English

If x ∈ y then y ∉ x for any x,y in Class.

Русский

Если x ∈ y, то y ∉ x для любых x,y в Class.

LaTeX

$$$\\\\forall {x y : Class}, \\\\mathrm{instMembership}.mem y x \\\\rightarrow \\\\neg \\\\mathrm{instMembership}.mem x y.$$$

Lean4

theorem mem_asymm {x y : Class} : x ∈ y → y ∉ x :=
  asymm_of (· ∈ ·)

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

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

Разделы

Аффилиация

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