inter_diff_distrib_right

Mathlib.Order.BooleanAlgebra.Set

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

English

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

Русский

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

LaTeX

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

Lean4

theorem inter_diff_distrib_right (s t u : Set α) : (s \ t) ∩ u = (s ∩ u) \ (t ∩ u) :=
  inf_sdiff_distrib_right _ _ _

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

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

Разделы

Аффилиация

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