diff_diff_right

Mathlib.Order.BooleanAlgebra.Set

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

English

For sets s,t,u, s \ (t \ u) = s \ t ∪ s ∩ u.

Русский

Для множеств S,T,U: S \ (T \ U) = S \ T ∪ S ∩ U.

LaTeX

$$$s \\ (t \\setminus u) = (s \\ t) \\cup (s \cap u)$$$

Lean4

theorem diff_diff_right {s t u : Set α} : s \ (t \ u) = s \ t ∪ s ∩ u :=
  sdiff_sdiff_right'

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

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

Разделы

Аффилиация

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