symmDiff_nonempty — Mathlib

English

The symmetric difference is nonempty if and only if the sets are distinct: (s Δ t).Nonempty ⇔ s ≠ t.

Русский

Симметрическая разность непустая тогда и только тогда, когда множества различны: (s Δ t).Nonempty ⇔ s ≠ t.

LaTeX

$$$ (s \\Delta t).Nonempty \\iff s \\neq t $$$

Lean4

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

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