Mathlib.Data.Finset.SymmDiff

Module docstring

{"# Symmetric difference of finite sets

This file concerns the symmetric difference operator s Δ t on finite sets.

Tags

finite sets, finset

","### Symmetric difference "}

Finset.mem_symmDiff theorem

: a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s

Full source

theorem mem_symmDiff : a ∈ s ∆ ta ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s := by
  simp_rw [symmDiff, sup_eq_union, mem_union, mem_sdiff]

Membership in Symmetric Difference of Finite Sets

Informal description

An element $a$ belongs to the symmetric difference $s \Delta t$ of two finite sets $s$ and $t$ if and only if $a$ is in $s$ but not in $t$, or $a$ is in $t$ but not in $s$. In symbols: $$ a \in s \Delta t \leftrightarrow (a \in s \land a \notin t) \lor (a \in t \land a \notin s) $$

Finset.coe_symmDiff theorem

: (↑(s ∆ t) : Set α) = (s : Set α) ∆ t

Full source

@[simp, norm_cast]
theorem coe_symmDiff : (↑(s ∆ t) : Set α) = (s : Set α) ∆ t :=
  Set.ext fun x => by simp [mem_symmDiff, Set.mem_symmDiff]

Coercion of Symmetric Difference from Finite Sets to Sets

Informal description

For any two finite sets $s$ and $t$ over a type $\alpha$, the symmetric difference $s \Delta t$ as a set (via the coercion from finite sets to sets) is equal to the symmetric difference of the sets $s$ and $t$. In symbols: $$ (s \Delta t : \text{Set } \alpha) = (s : \text{Set } \alpha) \Delta (t : \text{Set } \alpha) $$

Finset.symmDiff_eq_empty theorem

: s ∆ t = ∅ ↔ s = t

Full source

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

Symmetric Difference Vanishes if and Only if Sets Are Equal

Informal description

For any two finite sets $s$ and $t$, their symmetric difference $s \Delta t$ is empty if and only if $s = t$. In symbols: $$ s \Delta t = \emptyset \leftrightarrow s = t $$

Finset.symmDiff_nonempty theorem

: (s ∆ t).Nonempty ↔ s ≠ t

Full source

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

Nonempty Symmetric Difference Characterizes Inequality of Finite Sets

Informal description

For any two finite sets $s$ and $t$, their symmetric difference $s \Delta t$ is nonempty if and only if $s \neq t$. In symbols: $$ s \Delta t \neq \emptyset \leftrightarrow s \neq t $$

Finset.image_symmDiff theorem

[DecidableEq β] {f : α → β} (s t : Finset α) (hf : Injective f) : (s ∆ t).image f = s.image f ∆ t.image f

Full source

theorem image_symmDiff [DecidableEq β] {f : α → β} (s t : Finset α) (hf : Injective f) :
    (s ∆ t).image f = s.image f ∆ t.image f :=
  mod_cast Set.image_symmDiff hf s t

Image of Symmetric Difference Equals Symmetric Difference of Images for Finite Sets

Informal description

For any injective function $f : \alpha \to \beta$ and any finite sets $s, t \subseteq \alpha$, the image of their symmetric difference under $f$ equals the symmetric difference of their images. That is: $$ f(s \triangle t) = f(s) \triangle f(t). $$