doc-next-gen

Mathlib.Data.Set.SymmDiff

Module docstring

{"# Symmetric differences of sets "}

Set.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 :=
  Iff.rfl
Membership in Symmetric Difference of Sets
Informal description
An element $a$ belongs to the symmetric difference $s \Delta t$ of two 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 other words: $$ a \in s \Delta t \leftrightarrow (a \in s \land a \notin t) \lor (a \in t \land a \notin s). $$
Set.symmDiff_def theorem
(s t : Set α) : s ∆ t = s \ t ∪ t \ s
Full source 
protected theorem symmDiff_def (s t : Set α) : s ∆ t = s \ ts \ t ∪ t \ s :=
  rfl
Definition of Symmetric Difference via Set Differences
Informal description
For any two sets $s$ and $t$ in a type $\alpha$, their symmetric difference $s \triangle t$ is equal to the union of their set differences, i.e., $s \triangle t = (s \setminus t) \cup (t \setminus s)$.
Set.symmDiff_subset_union theorem
: s ∆ t ⊆ s ∪ t
Full source 
theorem symmDiff_subset_union : s ∆ ts ∆ t ⊆ s ∪ t :=
  @symmDiff_le_sup (Set α) _ _ _
Symmetric Difference is Subset of Union
Informal description
For any two sets $s$ and $t$ in a type $\alpha$, the symmetric difference $s \triangle t$ is a subset of their union $s \cup t$.
Set.symmDiff_eq_empty theorem
: s ∆ t = ∅ ↔ s = t
Full source 
@[simp]
theorem symmDiff_eq_empty : s ∆ ts ∆ t = ∅ ↔ s = t :=
  symmDiff_eq_bot
Symmetric Difference is Empty if and only if Sets are Equal
Informal description
For any two sets $s$ and $t$ in a type $\alpha$, the symmetric difference $s \triangle t$ is empty if and only if $s = t$.
Set.inter_symmDiff_distrib_left theorem
(s t u : Set α) : s ∩ t ∆ u = (s ∩ t) ∆ (s ∩ u)
Full source 
theorem inter_symmDiff_distrib_left (s t u : Set α) : s ∩ t ∆ u = (s ∩ t) ∆ (s ∩ u) :=
  inf_symmDiff_distrib_left _ _ _
Left Distributivity of Intersection over Symmetric Difference
Informal description
For any sets $s$, $t$, and $u$ in a type $\alpha$, the intersection of $s$ with the symmetric difference of $t$ and $u$ is equal to the symmetric difference of the intersections $s \cap t$ and $s \cap u$. In symbols: \[ s \cap (t \triangle u) = (s \cap t) \triangle (s \cap u). \]
Set.inter_symmDiff_distrib_right theorem
(s t u : Set α) : s ∆ t ∩ u = (s ∩ u) ∆ (t ∩ u)
Full source 
theorem inter_symmDiff_distrib_right (s t u : Set α) : s ∆ ts ∆ t ∩ u = (s ∩ u) ∆ (t ∩ u) :=
  inf_symmDiff_distrib_right _ _ _
Right Distributivity of Intersection over Symmetric Difference
Informal description
For any sets $s$, $t$, and $u$ in a type $\alpha$, the intersection of $u$ with the symmetric difference of $s$ and $t$ is equal to the symmetric difference of the intersections of $u$ with $s$ and $u$ with $t$. In symbols: \[ u \cap (s \triangle t) = (u \cap s) \triangle (u \cap t). \]
Set.subset_symmDiff_union_symmDiff_left theorem
(h : Disjoint s t) : u ⊆ s ∆ u ∪ t ∆ u
Full source 
theorem subset_symmDiff_union_symmDiff_left (h : Disjoint s t) : u ⊆ s ∆ u ∪ t ∆ u :=
  h.le_symmDiff_sup_symmDiff_left
Subset Property for Union of Symmetric Differences under Disjointness
Informal description
For any three sets $s$, $t$, and $u$ in a type $\alpha$, if $s$ and $t$ are disjoint, then $u$ is a subset of the union of the symmetric differences $s \triangle u$ and $t \triangle u$.