symmDiff_eq_empty

Mathlib.Data.Finset.SymmDiff

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

English

The symmetric difference is empty if and only if the two sets are equal.

Русский

Симметрическая разность пустая тогда и только тогда, когда множества равны.

LaTeX

$$$ s \\Delta t = \\emptyset \\iff s = t $$$

Lean4

@[simp]
theorem symmDiff_eq_empty : s ∆ t = ∅ ↔ s = t :=
  symmDiff_eq_bot

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

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

Разделы

Аффилиация

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