symmDiff_subset_sdiff

Mathlib.Data.Finset.SymmDiff

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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