union_diff_cancel'

Mathlib.Order.BooleanAlgebra.Set

URI: https://scilib.ai/kg/mathlib#Set.union_diff_cancel'

English

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

Русский

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

LaTeX

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

Lean4

theorem union_diff_cancel' {s t u : Set α} (h₁ : s ⊆ t) (h₂ : t ⊆ u) : t ∪ u \ s = u :=
  sup_sdiff_cancel' h₁ h₂

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

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

Разделы

Аффилиация

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