symmDiff_subset_sdiff'

Mathlib.Data.Finset.SymmDiff

URI: https://scilib.ai/kg/mathlib#Finset.symmDiff_subset_sdiff'

English

The right difference t \\ s is a subset of the symmetric difference s ∆ t.

Русский

Разность справа t \\ s является подмножеством симметрической разности s ∆ t.

LaTeX

$$$ t \\setminus s \\subseteq s \\Delta t $$$

Lean4

/-- See `symmDiff_subset_sdiff` for the swapped version of this. -/
theorem symmDiff_subset_sdiff' : t \ s ⊆ s ∆ t :=
  subset_union_right

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

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

Разделы

Аффилиация

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