diff_inter_distrib_right

Mathlib.Order.BooleanAlgebra.Set

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

English

Right distributivity of difference over intersection: (t ∩ r) \ s = (t \ s) ∩ (r \ s).

Русский

Правостороннее распределение разности над пересечением: (t ∩ r) \ s = (t \ s) ∩ (r \ s).

LaTeX

$$$ (t \cap r) \setminus s = (t \setminus s) \cap (r \setminus s).$$$

Lean4

theorem diff_inter_distrib_right (s t r : Set α) : (t ∩ r) \ s = (t \ s) ∩ (r \ s) :=
  inf_sdiff

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

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

Разделы

Аффилиация

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