symmetric_disjoint

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#symmetric_disjoint

English

The relation Disjoint is symmetric; equivalently the symmetric property holds for all a, b.

Русский

Отношение Disjoint симметрично; справедливо для любых a, b.

LaTeX

$$$Symmetric(Disjoint)$$$

Lean4

theorem symmetric_disjoint : Symmetric (Disjoint : α → α → Prop) :=
  Disjoint.symm

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

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

Разделы

Аффилиация

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