subset_diff_union

Mathlib.Order.BooleanAlgebra.Set

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

English

For sets s,t, s ⊆ s \ t ∪ t.

Русский

Для множеств S,T: S ⊆ S \ T ∪ T.

LaTeX

$$$(s \setminus t) \subseteq (s \setminus t) \,\\cup\, t$$$

Lean4

theorem subset_diff_union (s t : Set α) : s ⊆ s \ t ∪ t :=
  show s ≤ s \ t ∪ t from le_sdiff_sup

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

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

Разделы

Аффилиация

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