disjoint_comm

Mathlib.Order.Disjoint

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

English

Disjoint relation is symmetric: a disjoint b if and only if b is disjoint a.

Русский

Отношение взаимоисключения симметрично: Disjoint(a,b) эквивалентно Disjoint(b,a).

LaTeX

$$$Disjoint(a,b) \\iff Disjoint(b,a)$$$

Lean4

theorem disjoint_comm : Disjoint a b ↔ Disjoint b a :=
  forall_congr' fun _ ↦ forall_swap

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

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

Разделы

Аффилиация

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