symmDiff_eq_empty

Mathlib.Data.Set.SymmDiff

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

English

Symmetric difference is empty if and only if the two sets are equal: s ∆ t = ∅ ⇔ s = t.

Русский

Симметрическая разность пустая тогда и только тогда, когда множества равны: s ∆ t = ∅ ⇔ s = t.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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