disjoint_sdiff_sdiff

Mathlib.Order.BooleanAlgebra.Basic

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

English

The two skew differences are disjoint: (x \ y) and (y \ x) have empty intersection.

Русский

Два различия sdif друг другу не пересекаются: (x \ y) и (y \ x) имеют пустое пересечение.

LaTeX

$$$(x \setminus y) \wedge (y \setminus x) = \bot$$$

Lean4

theorem disjoint_sdiff_sdiff : Disjoint (x \ y) (y \ x) :=
  disjoint_iff_inf_le.mpr sdiff_inf_sdiff.le

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

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

Разделы

Аффилиация

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