inter_sdiff_left_comm

Mathlib.Order.BooleanAlgebra.Set

URI: https://scilib.ai/kg/mathlib#Set.inter_sdiff_left_comm

English

Left-commutativity of intersection and set difference: S ∩ (T \ U) = T ∩ (S \ U).

Русский

Левая перестановка пересечения и разности: S ∩ (T \ U) = T ∩ (S \ U).

LaTeX

$$$S \cap (T \setminus U) = T \cap (S \setminus U).$$$

Lean4

theorem inter_sdiff_left_comm (s t u : Set α) : s ∩ (t \ u) = t ∩ (s \ u) :=
  inf_sdiff_left_comm ..

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

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

Разделы

Аффилиация

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