HepLean Documentation
Mathlib
.
Data
.
Set
.
SymmDiff
Search
Google site search
return to top
source
Imports
Init
Mathlib.Order.Basic
Mathlib.Order.BooleanAlgebra
Mathlib.Order.SymmDiff
Mathlib.Tactic.ByContra
Mathlib.Tactic.Tauto
Mathlib.Util.Delaborators
Mathlib.Algebra.Group.ZeroOne
Mathlib.Data.Set.Basic
Mathlib.Data.Set.Operations
Mathlib.Logic.Equiv.Basic
Imported by
Set
.
mem_symmDiff
Set
.
symmDiff_def
Set
.
symmDiff_subset_union
Set
.
symmDiff_eq_empty
Set
.
symmDiff_nonempty
Set
.
inter_symmDiff_distrib_left
Set
.
inter_symmDiff_distrib_right
Set
.
subset_symmDiff_union_symmDiff_left
Set
.
subset_symmDiff_union_symmDiff_right
Symmetric differences of sets
#
source
theorem
Set
.
mem_symmDiff
{α :
Type
u}
{a :
α
}
{s t :
Set
α
}
:
a
∈
symmDiff
s
t
↔
a
∈
s
∧
a
∉
t
∨
a
∈
t
∧
a
∉
s
source
theorem
Set
.
symmDiff_def
{α :
Type
u}
(s t :
Set
α
)
:
symmDiff
s
t
=
s
\
t
∪
t
\
s
source
theorem
Set
.
symmDiff_subset_union
{α :
Type
u}
{s t :
Set
α
}
:
symmDiff
s
t
⊆
s
∪
t
source
@[simp]
theorem
Set
.
symmDiff_eq_empty
{α :
Type
u}
{s t :
Set
α
}
:
symmDiff
s
t
=
∅
↔
s
=
t
source
@[simp]
theorem
Set
.
symmDiff_nonempty
{α :
Type
u}
{s t :
Set
α
}
:
(
symmDiff
s
t
)
.Nonempty
↔
s
≠
t
source
theorem
Set
.
inter_symmDiff_distrib_left
{α :
Type
u}
(s t u :
Set
α
)
:
s
∩
symmDiff
t
u
=
symmDiff
(
s
∩
t
)
(
s
∩
u
)
source
theorem
Set
.
inter_symmDiff_distrib_right
{α :
Type
u}
(s t u :
Set
α
)
:
symmDiff
s
t
∩
u
=
symmDiff
(
s
∩
u
)
(
t
∩
u
)
source
theorem
Set
.
subset_symmDiff_union_symmDiff_left
{α :
Type
u}
{s t u :
Set
α
}
(h :
Disjoint
s
t
)
:
u
⊆
symmDiff
s
u
∪
symmDiff
t
u
source
theorem
Set
.
subset_symmDiff_union_symmDiff_right
{α :
Type
u}
{s t u :
Set
α
}
(h :
Disjoint
t
u
)
:
s
⊆
symmDiff
s
t
∪
symmDiff
s
u