symmDiff_subset_union

Mathlib.Data.Finset.SymmDiff

URI: https://scilib.ai/kg/mathlib#Finset.symmDiff_subset_union

English

The symmetric difference is contained in the union: s ∆ t ⊆ s ∪ t.

Русский

Симметрическая разность содержится в объединении: s ∆ t ⊆ s ∪ t.

LaTeX

$$$ s \\Delta t \\subseteq s \\cup t $$$

Lean4

theorem symmDiff_subset_union : s ∆ t ⊆ s ∪ t :=
  symmDiff_le_sup (α := Finset α)

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

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

Разделы

Аффилиация

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