symmDiff_nonempty

Mathlib.Data.Finset.SymmDiff

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

English

(s ∆ t) is nonempty iff s ≠ t.

Русский

Симметрическая разность непуста тогда и только тогда, когда s ≠ t.

LaTeX

$$$ (s \\Delta t).\\mathrm{Nonempty} \\iff s \\neq t $$$

Lean4

@[simp]
theorem symmDiff_nonempty : (s ∆ t).Nonempty ↔ s ≠ t :=
  nonempty_iff_ne_empty.trans symmDiff_eq_empty.not

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

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

Разделы

Аффилиация

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