symmDiff_eq_union_iff

Mathlib.Data.Finset.SymmDiff

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

English

Equality with union characterizes disjointness: s ∆ t = s ∪ t iff s and t are disjoint.

Русский

Равенство симметрической разности объединению эквивалентно тому, что s и t дизjoint.

LaTeX

$$$ (s \\Delta t) = (s \\cup t) \\iff Disjoint\\ s\\ t $$$

Lean4

theorem symmDiff_eq_union_iff (s t : Finset α) : s ∆ t = s ∪ t ↔ Disjoint s t :=
  symmDiff_eq_sup s t

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

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

Разделы

Аффилиация

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