symmDiff_subset_union

Mathlib.Data.Set.SymmDiff

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

English

Symmetric difference is always a subset of 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 (Set α) _ _ _

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

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

Разделы

Аффилиация

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