sdiff_inter_right_comm

Mathlib.Order.BooleanAlgebra.Set

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

English

Set difference commutes with intersection on the right: S \ (T ∩ U) = (S \ T) ∩ (S \ U).

Русский

Разность множеств с пересечением справа коммутирует: S \ (T ∩ U) = (S \ T) ∩ (S \ U).

LaTeX

$$$(S \ T) \ U = (S ∩ U) \ (T ∩ U).$$$

Lean4

/-- See also `Set.inter_diff_assoc`. -/
theorem sdiff_inter_right_comm (s t u : Set α) : s \ t ∩ u = (s ∩ u) \ t :=
  sdiff_inf_right_comm ..

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

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

Разделы

Аффилиация

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