disjoint_sdiff_comm

Mathlib.Order.BooleanAlgebra.Basic

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

English

Disjoint (x \ z) y ↔ Disjoint x (y \ z).

Русский

Disjoint (x \ z) y ↔ Disjoint x (y \ z).

LaTeX

$$$$ \mathrm{Disjoint}(x \setminus z, y) \iff \mathrm{Disjoint}(x, y \setminus z) $$$$

Lean4

theorem disjoint_sdiff_comm : Disjoint (x \ z) y ↔ Disjoint x (y \ z) := by
  simp_rw [disjoint_iff, sdiff_inf_right_comm, inf_sdiff_assoc]

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

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

Разделы

Аффилиация

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