diff_diff_eq_sdiff_union

Mathlib.Order.BooleanAlgebra.Set

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

English

If u ⊆ s, then s \ (t \ u) = (s \ t) ∪ u.

Русский

Если u ⊆ s, то s \ (t \ u) = (s \ t) ∪ u.

LaTeX

$$$(u \subseteq s) \Rightarrow s \setminus (t \setminus u) = (s \setminus t) \cup u$$$

Lean4

theorem diff_diff_eq_sdiff_union (h : u ⊆ s) : s \ (t \ u) = s \ t ∪ u :=
  sdiff_sdiff_eq_sdiff_sup h

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

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

Разделы

Аффилиация

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