inter_diff_assoc

Mathlib.Order.BooleanAlgebra.Set

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

English

Intersection distributes over set difference on the right: (A ∩ B) \ C = A ∩ (B \ C).

Русский

Пересечение распределяется по отношению к разности справа: (A ∩ B) \ C = A ∩ (B \ C).

LaTeX

$$$(A \ B) \ C = A \ (B \ C).$$$

Lean4

/-- See also `Set.sdiff_inter_right_comm`. -/
theorem inter_diff_assoc (a b c : Set α) : (a ∩ b) \ c = a ∩ (b \ c) :=
  inf_sdiff_assoc ..

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

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

Разделы

Аффилиация

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