Documentation

Mathlib.Order.BooleanAlgebra.Set

Boolean algebra of sets #

This file proves that Set α is a Boolean algebra, and proves results about set difference and complement.

Notation #

Tags #

set, sets, subset, subsets, complement

source
@[implicit_reducible]
instance Set.instHImp {α : Type u_1} :
HImp (Set α)
Equations
source
@[simp]
theorem Set.mem_himp_iff {α : Type u_1} {s t : Set α} {a : α} :
a ∈ s ⇨ t ↔ a ∈ s → a ∈ t
source
@[implicit_reducible]
instance Set.instBooleanAlgebra {α : Type u_1} :
BooleanAlgebra (Set α)
Equations
  • One or more equations did not get rendered due to their size.
source
theorem Set.himp_def {α : Type u_1} {s t : Set α} :
s ⇨ t = t ∪ sᶜ
source
theorem Set.inter_sdiff_assoc {α : Type u_1} (a b c : Set α) :
(a ∩ b) \ c = a ∩ (b \ c)

See also Set.sdiff_inter_right_comm.

source
@[deprecated Set.inter_sdiff_assoc (since := "2026-06-03")]
theorem Set.inter_diff_assoc {α : Type u_1} (a b c : Set α) :
(a ∩ b) \ c = a ∩ (b \ c)

Alias of Set.inter_sdiff_assoc.

See also Set.sdiff_inter_right_comm.

source
theorem Set.sdiff_inter_right_comm {α : Type u_1} (s t u : Set α) :
s \ t ∩ u = (s ∩ u) \ t

See also Set.inter_sdiff_assoc.

source
theorem Set.inter_sdiff_left_comm {α : Type u_1} (s t u : Set α) :
s ∩ (t \ u) = t ∩ (s \ u)
source
theorem Set.sdiff_union_sdiff_cancel {α : Type u_1} {s t u : Set α} (hts : t ⊆ s) (hut : u ⊆ t) :
s \ t ∪ t \ u = s \ u
source
@[deprecated Set.sdiff_union_sdiff_cancel (since := "2026-06-03")]
theorem Set.diff_union_diff_cancel {α : Type u_1} {s t u : Set α} (hts : t ⊆ s) (hut : u ⊆ t) :
s \ t ∪ t \ u = s \ u

Alias of Set.sdiff_union_sdiff_cancel.

source
theorem Set.sdiff_union_sdiff_cancel' {α : Type u_1} {s t u : Set α} (hi : s ∩ u ⊆ t) (hu : t ⊆ s ∪ u) :
s \ t ∪ t \ u = s \ u

A version of sdiff_union_sdiff_cancel with more general hypotheses.

source
@[deprecated Set.sdiff_union_sdiff_cancel' (since := "2026-06-03")]
theorem Set.diff_union_diff_cancel' {α : Type u_1} {s t u : Set α} (hi : s ∩ u ⊆ t) (hu : t ⊆ s ∪ u) :
s \ t ∪ t \ u = s \ u

Alias of Set.sdiff_union_sdiff_cancel'.

A version of sdiff_union_sdiff_cancel with more general hypotheses.

source
theorem Set.sdiff_sdiff_eq_sdiff_union {α : Type u_1} {s t u : Set α} (h : u ⊆ s) :
s \ (t \ u) = s \ t ∪ u
source
@[deprecated Set.sdiff_sdiff_eq_sdiff_union (since := "2026-06-03")]
theorem Set.diff_diff_eq_sdiff_union {α : Type u_1} {s t u : Set α} (h : u ⊆ s) :
s \ (t \ u) = s \ t ∪ u

Alias of Set.sdiff_sdiff_eq_sdiff_union.

source
theorem Set.inter_sdiff_distrib_left {α : Type u_1} (s t u : Set α) :
s ∩ (t \ u) = (s ∩ t) \ (s ∩ u)
source
@[deprecated Set.inter_sdiff_distrib_left (since := "2026-06-03")]
theorem Set.inter_diff_distrib_left {α : Type u_1} (s t u : Set α) :
s ∩ (t \ u) = (s ∩ t) \ (s ∩ u)

Alias of Set.inter_sdiff_distrib_left.

source
theorem Set.inter_sdiff_distrib_right {α : Type u_1} (s t u : Set α) :
s \ t ∩ u = (s ∩ u) \ (t ∩ u)
source
@[deprecated Set.inter_sdiff_distrib_right (since := "2026-06-03")]
theorem Set.inter_diff_distrib_right {α : Type u_1} (s t u : Set α) :
s \ t ∩ u = (s ∩ u) \ (t ∩ u)

Alias of Set.inter_sdiff_distrib_right.

source
theorem Set.sdiff_inter_distrib_right {α : Type u_1} (s t r : Set α) :
(t ∩ r) \ s = t \ s ∩ (r \ s)
source
@[deprecated Set.sdiff_inter_distrib_right (since := "2026-06-03")]
theorem Set.diff_inter_distrib_right {α : Type u_1} (s t r : Set α) :
(t ∩ r) \ s = t \ s ∩ (r \ s)

Alias of Set.sdiff_inter_distrib_right.

Lemmas about complement #

source
theorem Set.compl_def {α : Type u_1} (s : Set α) :
sᶜ = {x : α | ¬x ∈ s}
source
theorem Set.mem_compl {α : Type u_1} {s : Set α} {x : α} (h : ¬x ∈ s) :
x ∈ sᶜ
source
theorem Set.compl_setOf {α : Type u_3} (p : α → Prop) :
{a : α | p a}ᶜ = {a : α | ¬p a}
source
theorem Set.notMem_of_mem_compl {α : Type u_1} {s : Set α} {x : α} (h : x ∈ sᶜ) :
¬x ∈ s
source
theorem Set.notMem_compl_iff {α : Type u_1} {s : Set α} {x : α} :
¬x ∈ sᶜ ↔ x ∈ s
source
@[simp]
theorem Set.inter_compl_self {α : Type u_1} (s : Set α) :
s ∩ sᶜ = ∅
source
@[simp]
theorem Set.compl_inter_self {α : Type u_1} (s : Set α) :
sᶜ ∩ s = ∅
source
@[simp]
theorem Set.compl_empty {α : Type u_1} :
∅ᶜ = univ
source
@[simp]
theorem Set.compl_union {α : Type u_1} (s t : Set α) :
(s ∪ t)ᶜ = sᶜ ∩ tᶜ
source
theorem Set.compl_inter {α : Type u_1} (s t : Set α) :
(s ∩ t)ᶜ = sᶜ ∪ tᶜ
source
@[simp]
theorem Set.compl_univ {α : Type u_1} :
univᶜ = ∅
source
@[simp]
theorem Set.compl_empty_iff {α : Type u_1} {s : Set α} :
sᶜ = ∅ ↔ s = univ
source
@[simp]
theorem Set.compl_univ_iff {α : Type u_1} {s : Set α} :
sᶜ = univ ↔ s = ∅
source
theorem Set.compl_ne_univ {α : Type u_1} {s : Set α} :
sᶜ ≠ univ ↔ s.Nonempty
source
theorem Set.inl_compl_union_inr_compl {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
Sum.inl '' sᶜ ∪ Sum.inr '' tᶜ = (Sum.inl '' s ∪ Sum.inr '' t)ᶜ
source
theorem Set.nonempty_compl {α : Type u_1} {s : Set α} :
sᶜ.Nonempty ↔ s ≠ univ
source
theorem Set.union_eq_compl_compl_inter_compl {α : Type u_1} (s t : Set α) :
s ∪ t = (sᶜ ∩ tᶜ)ᶜ
source
theorem Set.inter_eq_compl_compl_union_compl {α : Type u_1} (s t : Set α) :
s ∩ t = (sᶜ ∪ tᶜ)ᶜ
source
@[simp]
theorem Set.union_compl_self {α : Type u_1} (s : Set α) :
s ∪ sᶜ = univ
source
@[simp]
theorem Set.compl_union_self {α : Type u_1} (s : Set α) :
sᶜ ∪ s = univ
source
theorem Set.compl_subset_comm {α : Type u_1} {s t : Set α} :
sᶜ ⊆ t ↔ tᶜ ⊆ s
source
theorem Set.subset_compl_comm {α : Type u_1} {s t : Set α} :
s ⊆ tᶜ ↔ t ⊆ sᶜ
source
@[simp]
theorem Set.compl_subset_compl {α : Type u_1} {s t : Set α} :
sᶜ ⊆ tᶜ ↔ t ⊆ s
source
theorem Set.compl_subset_compl_of_subset {α : Type u_1} {s t : Set α} (h : t ⊆ s) :
sᶜ ⊆ tᶜ
source
theorem Set.subset_union_compl_iff_inter_subset {α : Type u_1} {s t u : Set α} :
s ⊆ t ∪ uᶜ ↔ s ∩ u ⊆ t
source
theorem Set.compl_subset_iff_union {α : Type u_1} {s t : Set α} :
sᶜ ⊆ t ↔ s ∪ t = univ
source
theorem Set.inter_subset {α : Type u_1} (a b c : Set α) :
a ∩ b ⊆ c ↔ a ⊆ bᶜ ∪ c
source
theorem Set.inter_compl_nonempty_iff {α : Type u_1} {s t : Set α} :
(s ∩ tᶜ).Nonempty ↔ ¬s ⊆ t
source
theorem Set.subset_compl_iff_disjoint_left {α : Type u_1} {s t : Set α} :
s ⊆ tᶜ ↔ Disjoint t s
source
theorem Set.subset_compl_iff_disjoint_right {α : Type u_1} {s t : Set α} :
s ⊆ tᶜ ↔ Disjoint s t
source
theorem Set.disjoint_compl_left_iff_subset {α : Type u_1} {s t : Set α} :
Disjoint sᶜ t ↔ t ⊆ s
source
theorem Set.disjoint_compl_right_iff_subset {α : Type u_1} {s t : Set α} :
Disjoint s tᶜ ↔ s ⊆ t
source
theorem Disjoint.subset_compl_right {α : Type u_1} {s t : Set α} :
Disjoint s t → s ⊆ tᶜ

Alias of the reverse direction of Set.subset_compl_iff_disjoint_right.

source
theorem Disjoint.subset_compl_left {α : Type u_1} {s t : Set α} :
Disjoint t s → s ⊆ tᶜ

Alias of the reverse direction of Set.subset_compl_iff_disjoint_left.

source
theorem HasSubset.Subset.disjoint_compl_left {α : Type u_1} {s t : Set α} :
t ⊆ s → Disjoint sᶜ t

Alias of the reverse direction of Set.disjoint_compl_left_iff_subset.

source
theorem HasSubset.Subset.disjoint_compl_right {α : Type u_1} {s t : Set α} :
s ⊆ t → Disjoint s tᶜ

Alias of the reverse direction of Set.disjoint_compl_right_iff_subset.

source
@[simp]
theorem Set.nonempty_compl_of_nontrivial {α : Type u_1} [Nontrivial α] (x : α) :
{x}ᶜ.Nonempty
source
theorem Set.mem_compl_singleton_iff {α : Type u_1} {a b : α} :
a ∈ {b}ᶜ ↔ a ≠ b
source
theorem Set.compl_singleton_eq {α : Type u_1} (a : α) :
{a}ᶜ = {x : α | x ≠ a}
source
@[simp]
theorem Set.compl_ne_eq_singleton {α : Type u_1} (a : α) :
{x : α | x ≠ a}ᶜ = {a}
source
@[simp]
theorem Set.subset_compl_singleton_iff {α : Type u_1} {s : Set α} {a : α} :
s ⊆ {a}ᶜ ↔ ¬a ∈ s

Lemmas about set difference #

source
theorem Set.notMem_sdiff_of_mem {α : Type u_1} {s t : Set α} {x : α} (hx : x ∈ t) :
¬x ∈ s \ t
source
@[deprecated Set.notMem_sdiff_of_mem (since := "2026-06-03")]
theorem Set.notMem_diff_of_mem {α : Type u_1} {s t : Set α} {x : α} (hx : x ∈ t) :
¬x ∈ s \ t

Alias of Set.notMem_sdiff_of_mem.

source
theorem Set.mem_of_mem_sdiff {α : Type u_1} {s t : Set α} {x : α} (h : x ∈ s \ t) :
x ∈ s
source
@[deprecated Set.mem_of_mem_sdiff (since := "2026-06-03")]
theorem Set.mem_of_mem_diff {α : Type u_1} {s t : Set α} {x : α} (h : x ∈ s \ t) :
x ∈ s

Alias of Set.mem_of_mem_sdiff.

source
theorem Set.notMem_of_mem_sdiff {α : Type u_1} {s t : Set α} {x : α} (h : x ∈ s \ t) :
¬x ∈ t
source
@[deprecated Set.notMem_of_mem_sdiff (since := "2026-06-03")]
theorem Set.notMem_of_mem_diff {α : Type u_1} {s t : Set α} {x : α} (h : x ∈ s \ t) :
¬x ∈ t

Alias of Set.notMem_of_mem_sdiff.

source
theorem Set.sdiff_eq_compl_inter {α : Type u_1} {s t : Set α} :
s \ t = tᶜ ∩ s
source
@[deprecated Set.sdiff_eq_compl_inter (since := "2026-06-03")]
theorem Set.diff_eq_compl_inter {α : Type u_1} {s t : Set α} :
s \ t = tᶜ ∩ s

Alias of Set.sdiff_eq_compl_inter.

source
theorem Set.sdiff_nonempty {α : Type u_1} {s t : Set α} :
(s \ t).Nonempty ↔ ¬s ⊆ t
source
@[deprecated Set.sdiff_nonempty (since := "2026-06-03")]
theorem Set.diff_nonempty {α : Type u_1} {s t : Set α} :
(s \ t).Nonempty ↔ ¬s ⊆ t

Alias of Set.sdiff_nonempty.

source
theorem Set.sdiff_subset {α : Type u_1} {s t : Set α} :
s \ t ⊆ s
source
@[deprecated Set.sdiff_subset (since := "2026-06-03")]
theorem Set.diff_subset {α : Type u_1} {s t : Set α} :
s \ t ⊆ s

Alias of Set.sdiff_subset.

source
theorem Set.sdiff_subset_compl {α : Type u_1} (s t : Set α) :
s \ t ⊆ tᶜ
source
@[deprecated Set.sdiff_subset_compl (since := "2026-06-03")]
theorem Set.diff_subset_compl {α : Type u_1} (s t : Set α) :
s \ t ⊆ tᶜ

Alias of Set.sdiff_subset_compl.

source
theorem Set.union_sdiff_cancel' {α : Type u_1} {s t u : Set α} (h₁ : s ⊆ t) (h₂ : t ⊆ u) :
t ∪ u \ s = u
source
@[deprecated Set.union_sdiff_cancel' (since := "2026-06-03")]
theorem Set.union_diff_cancel' {α : Type u_1} {s t u : Set α} (h₁ : s ⊆ t) (h₂ : t ⊆ u) :
t ∪ u \ s = u

Alias of Set.union_sdiff_cancel'.

source
theorem Set.union_sdiff_cancel {α : Type u_1} {s t : Set α} (h : s ⊆ t) :
s ∪ t \ s = t
source
@[deprecated Set.union_sdiff_cancel (since := "2026-06-03")]
theorem Set.union_diff_cancel {α : Type u_1} {s t : Set α} (h : s ⊆ t) :
s ∪ t \ s = t

Alias of Set.union_sdiff_cancel.

source
theorem Set.union_sdiff_cancel_left {α : Type u_1} {s t : Set α} (h : s ∩ t ⊆ ∅) :
(s ∪ t) \ s = t
source
@[deprecated Set.union_sdiff_cancel_left (since := "2026-06-03")]
theorem Set.union_diff_cancel_left {α : Type u_1} {s t : Set α} (h : s ∩ t ⊆ ∅) :
(s ∪ t) \ s = t

Alias of Set.union_sdiff_cancel_left.

source
theorem Set.union_sdiff_cancel_right {α : Type u_1} {s t : Set α} (h : s ∩ t ⊆ ∅) :
(s ∪ t) \ t = s
source
@[deprecated Set.union_sdiff_cancel_right (since := "2026-06-03")]
theorem Set.union_diff_cancel_right {α : Type u_1} {s t : Set α} (h : s ∩ t ⊆ ∅) :
(s ∪ t) \ t = s

Alias of Set.union_sdiff_cancel_right.

source
@[simp]
theorem Set.union_sdiff_left {α : Type u_1} {s t : Set α} :
(s ∪ t) \ s = t \ s
source
@[deprecated Set.union_sdiff_left (since := "2026-06-03")]
theorem Set.union_diff_left {α : Type u_1} {s t : Set α} :
(s ∪ t) \ s = t \ s

Alias of Set.union_sdiff_left.

source
@[simp]
theorem Set.union_sdiff_right {α : Type u_1} {s t : Set α} :
(s ∪ t) \ t = s \ t
source
@[deprecated Set.union_sdiff_right (since := "2026-06-03")]
theorem Set.union_diff_right {α : Type u_1} {s t : Set α} :
(s ∪ t) \ t = s \ t

Alias of Set.union_sdiff_right.

source
theorem Set.union_sdiff_distrib {α : Type u_1} {s t u : Set α} :
(s ∪ t) \ u = s \ u ∪ t \ u
source
@[deprecated Set.union_sdiff_distrib (since := "2026-06-03")]
theorem Set.union_diff_distrib {α : Type u_1} {s t u : Set α} :
(s ∪ t) \ u = s \ u ∪ t \ u

Alias of Set.union_sdiff_distrib.

source
@[simp]
theorem Set.inter_sdiff_self {α : Type u_1} (a b : Set α) :
a ∩ (b \ a) = ∅
source
@[deprecated Set.inter_sdiff_self (since := "2026-06-03")]
theorem Set.inter_diff_self {α : Type u_1} (a b : Set α) :
a ∩ (b \ a) = ∅

Alias of Set.inter_sdiff_self.

source
@[simp]
theorem Set.inter_union_sdiff {α : Type u_1} (s t : Set α) :
s ∩ t ∪ s \ t = s
source
@[deprecated Set.inter_union_sdiff (since := "2026-06-03")]
theorem Set.inter_union_diff {α : Type u_1} (s t : Set α) :
s ∩ t ∪ s \ t = s

Alias of Set.inter_union_sdiff.

source
@[simp]
theorem Set.sdiff_union_inter {α : Type u_1} (s t : Set α) :
s \ t ∪ s ∩ t = s
source
@[deprecated Set.sdiff_union_inter (since := "2026-06-03")]
theorem Set.diff_union_inter {α : Type u_1} (s t : Set α) :
s \ t ∪ s ∩ t = s

Alias of Set.sdiff_union_inter.

source
@[simp]
theorem Set.inter_union_compl {α : Type u_1} (s t : Set α) :
s ∩ t ∪ s ∩ tᶜ = s
source
theorem Set.subset_inter_union_compl_left {α : Type u_1} (s t : Set α) :
t ⊆ s ∩ t ∪ sᶜ
source
theorem Set.subset_inter_union_compl_right {α : Type u_1} (s t : Set α) :
s ⊆ s ∩ t ∪ tᶜ
source
theorem Set.union_inter_compl_left_subset {α : Type u_1} (s t : Set α) :
(s ∪ t) ∩ sᶜ ⊆ t
source
theorem Set.union_inter_compl_right_subset {α : Type u_1} (s t : Set α) :
(s ∪ t) ∩ tᶜ ⊆ s
source
theorem Set.sdiff_subset_sdiff {α : Type u_1} {s₁ s₂ t₁ t₂ : Set α} :
s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂
source
@[deprecated Set.sdiff_subset_sdiff (since := "2026-06-03")]
theorem Set.diff_subset_diff {α : Type u_1} {s₁ s₂ t₁ t₂ : Set α} :
s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂

Alias of Set.sdiff_subset_sdiff.

source
theorem Set.sdiff_subset_sdiff_left {α : Type u_1} {s₁ s₂ t : Set α} (h : s₁ ⊆ s₂) :
s₁ \ t ⊆ s₂ \ t
source
@[deprecated Set.sdiff_subset_sdiff_left (since := "2026-06-03")]
theorem Set.diff_subset_diff_left {α : Type u_1} {s₁ s₂ t : Set α} (h : s₁ ⊆ s₂) :
s₁ \ t ⊆ s₂ \ t

Alias of Set.sdiff_subset_sdiff_left.

source
theorem Set.sdiff_subset_sdiff_right {α : Type u_1} {s t u : Set α} (h : t ⊆ u) :
s \ u ⊆ s \ t
source
@[deprecated Set.sdiff_subset_sdiff_right (since := "2026-06-03")]
theorem Set.diff_subset_diff_right {α : Type u_1} {s t u : Set α} (h : t ⊆ u) :
s \ u ⊆ s \ t

Alias of Set.sdiff_subset_sdiff_right.

source
theorem Set.sdiff_subset_sdiff_iff_subset {α : Type u_1} {s t r : Set α} (hs : s ⊆ r) (ht : t ⊆ r) :
r \ s ⊆ r \ t ↔ t ⊆ s
source
@[deprecated Set.sdiff_subset_sdiff_iff_subset (since := "2026-06-03")]
theorem Set.diff_subset_diff_iff_subset {α : Type u_1} {s t r : Set α} (hs : s ⊆ r) (ht : t ⊆ r) :
r \ s ⊆ r \ t ↔ t ⊆ s

Alias of Set.sdiff_subset_sdiff_iff_subset.

source
theorem Set.compl_eq_univ_sdiff {α : Type u_1} (s : Set α) :
sᶜ = univ \ s
source
@[deprecated Set.compl_eq_univ_sdiff (since := "2026-06-03")]
theorem Set.compl_eq_univ_diff {α : Type u_1} (s : Set α) :
sᶜ = univ \ s

Alias of Set.compl_eq_univ_sdiff.

source
@[simp]
theorem Set.empty_sdiff {α : Type u_1} (s : Set α) :
∅ \ s = ∅
source
@[deprecated Set.empty_sdiff (since := "2026-06-03")]
theorem Set.empty_diff {α : Type u_1} (s : Set α) :
∅ \ s = ∅

Alias of Set.empty_sdiff.

source
theorem Set.sdiff_eq_empty {α : Type u_1} {s t : Set α} :
s \ t = ∅ ↔ s ⊆ t
source
@[deprecated Set.sdiff_eq_empty (since := "2026-06-03")]
theorem Set.diff_eq_empty {α : Type u_1} {s t : Set α} :
s \ t = ∅ ↔ s ⊆ t

Alias of Set.sdiff_eq_empty.

source
@[simp]
theorem Set.sdiff_empty {α : Type u_1} {s : Set α} :
s \ ∅ = s
source
@[deprecated Set.sdiff_empty (since := "2026-06-03")]
theorem Set.diff_empty {α : Type u_1} {s : Set α} :
s \ ∅ = s

Alias of Set.sdiff_empty.

source
@[simp]
theorem Set.sdiff_univ {α : Type u_1} (s : Set α) :
s \ univ = ∅
source
@[deprecated Set.sdiff_univ (since := "2026-06-03")]
theorem Set.diff_univ {α : Type u_1} (s : Set α) :
s \ univ = ∅

Alias of Set.sdiff_univ.

source
theorem Set.sdiff_sdiff {α : Type u_1} {s t u : Set α} :
(s \ t) \ u = s \ (t ∪ u)
source
@[deprecated Set.sdiff_sdiff (since := "2026-06-03")]
theorem Set.diff_diff {α : Type u_1} {s t u : Set α} :
(s \ t) \ u = s \ (t ∪ u)

Alias of Set.sdiff_sdiff.

source
theorem Set.sdiff_sdiff_comm {α : Type u_1} {s t u : Set α} :
(s \ t) \ u = (s \ u) \ t
source
@[deprecated Set.sdiff_sdiff_comm (since := "2026-06-03")]
theorem Set.diff_diff_comm {α : Type u_1} {s t u : Set α} :
(s \ t) \ u = (s \ u) \ t

Alias of Set.sdiff_sdiff_comm.

source
@[simp]
theorem Set.sdiff_subset_iff {α : Type u_1} {s t u : Set α} :
s \ t ⊆ u ↔ s ⊆ t ∪ u
source
@[deprecated Set.sdiff_subset_iff (since := "2026-06-03")]
theorem Set.diff_subset_iff {α : Type u_1} {s t u : Set α} :
s \ t ⊆ u ↔ s ⊆ t ∪ u

Alias of Set.sdiff_subset_iff.

source
theorem Set.subset_sdiff_union {α : Type u_1} (s t : Set α) :
s ⊆ s \ t ∪ t
source
@[deprecated Set.subset_sdiff_union (since := "2026-06-03")]
theorem Set.subset_diff_union {α : Type u_1} (s t : Set α) :
s ⊆ s \ t ∪ t

Alias of Set.subset_sdiff_union.

source
theorem Set.sdiff_union_of_subset {α : Type u_1} {s t : Set α} (h : t ⊆ s) :
s \ t ∪ t = s
source
@[deprecated Set.sdiff_union_of_subset (since := "2026-06-03")]
theorem Set.diff_union_of_subset {α : Type u_1} {s t : Set α} (h : t ⊆ s) :
s \ t ∪ t = s

Alias of Set.sdiff_union_of_subset.

source
theorem Set.sdiff_subset_comm {α : Type u_1} {s t u : Set α} :
s \ t ⊆ u ↔ s \ u ⊆ t
source
@[deprecated Set.sdiff_subset_comm (since := "2026-06-03")]
theorem Set.diff_subset_comm {α : Type u_1} {s t u : Set α} :
s \ t ⊆ u ↔ s \ u ⊆ t

Alias of Set.sdiff_subset_comm.

source
theorem Set.sdiff_inter {α : Type u_1} {s t u : Set α} :
s \ (t ∩ u) = s \ t ∪ s \ u
source
@[deprecated Set.sdiff_inter (since := "2026-06-03")]
theorem Set.diff_inter {α : Type u_1} {s t u : Set α} :
s \ (t ∩ u) = s \ t ∪ s \ u

Alias of Set.sdiff_inter.

source
theorem Set.sdiff_inter_sdiff {α : Type u_1} {s t u : Set α} :
s \ t ∩ (s \ u) = s \ (t ∪ u)
source
@[deprecated Set.sdiff_inter_sdiff (since := "2026-06-03")]
theorem Set.diff_inter_diff {α : Type u_1} {s t u : Set α} :
s \ t ∩ (s \ u) = s \ (t ∪ u)

Alias of Set.sdiff_inter_sdiff.

source
theorem Set.sdiff_compl {α : Type u_1} {s t : Set α} :
s \ tᶜ = s ∩ t
source
@[deprecated Set.sdiff_compl (since := "2026-06-03")]
theorem Set.diff_compl {α : Type u_1} {s t : Set α} :
s \ tᶜ = s ∩ t

Alias of Set.sdiff_compl.

source
theorem Set.compl_sdiff {α : Type u_1} {s t : Set α} :
(t \ s)ᶜ = s ∪ tᶜ
source
@[deprecated Set.compl_sdiff (since := "2026-06-03")]
theorem Set.compl_diff {α : Type u_1} {s t : Set α} :
(t \ s)ᶜ = s ∪ tᶜ

Alias of Set.compl_sdiff.

source
theorem Set.sdiff_sdiff_right {α : Type u_1} {s t u : Set α} :
s \ (t \ u) = s \ t ∪ s ∩ u
source
@[deprecated Set.sdiff_sdiff_right (since := "2026-06-03")]
theorem Set.diff_diff_right {α : Type u_1} {s t u : Set α} :
s \ (t \ u) = s \ t ∪ s ∩ u

Alias of Set.sdiff_sdiff_right.

source
theorem Set.inter_sdiff_right_comm {α : Type u_1} {s t u : Set α} :
(s ∩ t) \ u = s \ u ∩ t
source
@[deprecated Set.inter_sdiff_right_comm (since := "2026-06-03")]
theorem Set.diff_inter_right_comm {α : Type u_1} {s t u : Set α} :
(s ∩ t) \ u = s \ u ∩ t

Alias of Set.inter_sdiff_right_comm.

source
@[simp]
theorem Set.union_sdiff_self {α : Type u_1} {s t : Set α} :
s ∪ t \ s = s ∪ t
source
@[deprecated Set.union_sdiff_self (since := "2026-06-03")]
theorem Set.union_diff_self {α : Type u_1} {s t : Set α} :
s ∪ t \ s = s ∪ t

Alias of Set.union_sdiff_self.

source
@[simp]
theorem Set.sdiff_union_self {α : Type u_1} {s t : Set α} :
s \ t ∪ t = s ∪ t
source
@[deprecated Set.sdiff_union_self (since := "2026-06-03")]
theorem Set.diff_union_self {α : Type u_1} {s t : Set α} :
s \ t ∪ t = s ∪ t

Alias of Set.sdiff_union_self.

source
@[simp]
theorem Set.sdiff_inter_self {α : Type u_1} {a b : Set α} :
b \ a ∩ a = ∅
source
@[deprecated Set.sdiff_inter_self (since := "2026-06-03")]
theorem Set.diff_inter_self {α : Type u_1} {a b : Set α} :
b \ a ∩ a = ∅

Alias of Set.sdiff_inter_self.

source
@[simp]
theorem Set.sdiff_inter_self_eq_sdiff {α : Type u_1} {s t : Set α} :
s \ (t ∩ s) = s \ t
source
@[deprecated Set.sdiff_inter_self_eq_sdiff (since := "2026-06-03")]
theorem Set.diff_inter_self_eq_diff {α : Type u_1} {s t : Set α} :
s \ (t ∩ s) = s \ t

Alias of Set.sdiff_inter_self_eq_sdiff.

source
@[simp]
theorem Set.sdiff_self_inter {α : Type u_1} {s t : Set α} :
s \ (s ∩ t) = s \ t
source
@[deprecated Set.sdiff_self_inter (since := "2026-06-03")]
theorem Set.diff_self_inter {α : Type u_1} {s t : Set α} :
s \ (s ∩ t) = s \ t

Alias of Set.sdiff_self_inter.

source
theorem Set.sdiff_self {α : Type u_1} {s : Set α} :
s \ s = ∅
source
@[deprecated Set.sdiff_self (since := "2026-06-03")]
theorem Set.diff_self {α : Type u_1} {s : Set α} :
s \ s = ∅

Alias of Set.sdiff_self.

source
theorem Set.sdiff_sdiff_right_self {α : Type u_1} (s t : Set α) :
s \ (s \ t) = s ∩ t
source
@[deprecated Set.sdiff_sdiff_right_self (since := "2026-06-03")]
theorem Set.diff_diff_right_self {α : Type u_1} (s t : Set α) :
s \ (s \ t) = s ∩ t

Alias of Set.sdiff_sdiff_right_self.

source
theorem Set.sdiff_sdiff_cancel_left {α : Type u_1} {s t : Set α} (h : s ⊆ t) :
t \ (t \ s) = s
source
@[deprecated Set.sdiff_sdiff_cancel_left (since := "2026-06-03")]
theorem Set.diff_diff_cancel_left {α : Type u_1} {s t : Set α} (h : s ⊆ t) :
t \ (t \ s) = s

Alias of Set.sdiff_sdiff_cancel_left.

source
theorem Set.union_eq_sdiff_union_sdiff_union_inter {α : Type u_1} (s t : Set α) :
s ∪ t = s \ t ∪ t \ s ∪ s ∩ t
source
@[deprecated Set.union_eq_sdiff_union_sdiff_union_inter (since := "2026-06-03")]
theorem Set.union_eq_diff_union_diff_union_inter {α : Type u_1} (s t : Set α) :
s ∪ t = s \ t ∪ t \ s ∪ s ∩ t

Alias of Set.union_eq_sdiff_union_sdiff_union_inter.

source
@[simp]
theorem Set.sdiff_sep_self {α : Type u_1} (s : Set α) (p : α → Prop) :
s \ {a : α | a ∈ s ∧ p a} = {a : α | a ∈ s ∧ ¬p a}
source
theorem Set.disjoint_sdiff_left {α : Type u_1} {s t : Set α} :
Disjoint (t \ s) s
source
theorem Set.disjoint_sdiff_right {α : Type u_1} {s t : Set α} :
Disjoint s (t \ s)
source
theorem Set.disjoint_sdiff_inter {α : Type u_1} {s t : Set α} :
Disjoint (s \ t) (s ∩ t)
source
theorem Set.subset_sdiff {α : Type u_1} {s t u : Set α} :
s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u
source
@[deprecated Set.subset_sdiff (since := "2026-06-03")]
theorem Set.subset_diff {α : Type u_1} {s t u : Set α} :
s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u

Alias of Set.subset_sdiff.

source
theorem Set.disjoint_of_subset_iff_left_eq_empty {α : Type u_1} {s t : Set α} (h : s ⊆ t) :
Disjoint s t ↔ s = ∅
source
@[simp]
theorem Set.sdiff_ssubset_left_iff {α : Type u_1} {s t : Set α} :
s \ t ⊂ s ↔ (s ∩ t).Nonempty
source
@[deprecated Set.sdiff_ssubset_left_iff (since := "2026-06-03")]
theorem Set.diff_ssubset_left_iff {α : Type u_1} {s t : Set α} :
s \ t ⊂ s ↔ (s ∩ t).Nonempty

Alias of Set.sdiff_ssubset_left_iff.

source
theorem HasSubset.Subset.sdiff_ssubset_of_nonempty {α : Type u_1} {s t : Set α} (hst : s ⊆ t) (hs : s.Nonempty) :
t \ s ⊂ t
source
@[deprecated HasSubset.Subset.sdiff_ssubset_of_nonempty (since := "2026-06-03")]
theorem HasSubset.Subset.diff_ssubset_of_nonempty {α : Type u_1} {s t : Set α} (hst : s ⊆ t) (hs : s.Nonempty) :
t \ s ⊂ t

Alias of HasSubset.Subset.sdiff_ssubset_of_nonempty.

source
theorem Set.ssubset_iff_sdiff_singleton {α : Type u_1} {s t : Set α} :
s ⊂ t ↔ ∃ (a : α), a ∈ t ∧ s ⊆ t \ {a}
source
theorem Set.sdiff_singleton_subset_iff {α : Type u_1} {s t : Set α} {a : α} :
s \ {a} ⊆ t ↔ s ⊆ insert a t
source
@[deprecated Set.sdiff_singleton_subset_iff (since := "2026-06-03")]
theorem Set.diff_singleton_subset_iff {α : Type u_1} {s t : Set α} {a : α} :
s \ {a} ⊆ t ↔ s ⊆ insert a t

Alias of Set.sdiff_singleton_subset_iff.

source
theorem Set.subset_sdiff_singleton {α : Type u_1} {s t : Set α} {a : α} (h : s ⊆ t) (ha : ¬a ∈ s) :
s ⊆ t \ {a}
source
@[deprecated Set.subset_sdiff_singleton (since := "2026-06-03")]
theorem Set.subset_diff_singleton {α : Type u_1} {s t : Set α} {a : α} (h : s ⊆ t) (ha : ¬a ∈ s) :
s ⊆ t \ {a}

Alias of Set.subset_sdiff_singleton.

source
theorem Set.subset_insert_sdiff_singleton {α : Type u_1} (x : α) (s : Set α) :
s ⊆ insert x (s \ {x})
source
@[deprecated Set.subset_insert_sdiff_singleton (since := "2026-06-03")]
theorem Set.subset_insert_diff_singleton {α : Type u_1} (x : α) (s : Set α) :
s ⊆ insert x (s \ {x})

Alias of Set.subset_insert_sdiff_singleton.

source
theorem Set.sdiff_insert_of_notMem {α : Type u_1} {s t : Set α} {a : α} (h : ¬a ∈ s) :
s \ insert a t = s \ t
source
@[deprecated Set.sdiff_insert_of_notMem (since := "2026-06-03")]
theorem Set.diff_insert_of_notMem {α : Type u_1} {s t : Set α} {a : α} (h : ¬a ∈ s) :
s \ insert a t = s \ t

Alias of Set.sdiff_insert_of_notMem.

source
@[simp]
theorem Set.insert_sdiff_of_mem {α : Type u_1} {t : Set α} {a : α} (s : Set α) (h : a ∈ t) :
insert a s \ t = s \ t
source
@[deprecated Set.insert_sdiff_of_mem (since := "2026-06-03")]
theorem Set.insert_diff_of_mem {α : Type u_1} {t : Set α} {a : α} (s : Set α) (h : a ∈ t) :
insert a s \ t = s \ t

Alias of Set.insert_sdiff_of_mem.

source
theorem Set.insert_sdiff_of_notMem {α : Type u_1} {t : Set α} {a : α} (s : Set α) (h : ¬a ∈ t) :
insert a s \ t = insert a (s \ t)
source
@[deprecated Set.insert_sdiff_of_notMem (since := "2026-06-03")]
theorem Set.insert_diff_of_notMem {α : Type u_1} {t : Set α} {a : α} (s : Set α) (h : ¬a ∈ t) :
insert a s \ t = insert a (s \ t)

Alias of Set.insert_sdiff_of_notMem.

source
theorem Set.insert_sdiff_self_of_notMem {α : Type u_1} {s : Set α} {a : α} (h : ¬a ∈ s) :
insert a s \ {a} = s
source
@[deprecated Set.insert_sdiff_self_of_notMem (since := "2026-06-03")]
theorem Set.insert_diff_self_of_notMem {α : Type u_1} {s : Set α} {a : α} (h : ¬a ∈ s) :
insert a s \ {a} = s

Alias of Set.insert_sdiff_self_of_notMem.

source
@[simp]
theorem Set.insert_sdiff_self_of_mem {α : Type u_1} {s : Set α} {a : α} (ha : a ∈ s) :
insert a (s \ {a}) = s
source
@[deprecated Set.insert_sdiff_self_of_mem (since := "2026-06-03")]
theorem Set.insert_diff_self_of_mem {α : Type u_1} {s : Set α} {a : α} (ha : a ∈ s) :
insert a (s \ {a}) = s

Alias of Set.insert_sdiff_self_of_mem.

source
theorem Set.insert_sdiff_subset {α : Type u_1} {s t : Set α} {a : α} :
insert a s \ t ⊆ insert a (s \ t)
source
@[deprecated Set.insert_sdiff_subset (since := "2026-06-03")]
theorem Set.insert_diff_subset {α : Type u_1} {s t : Set α} {a : α} :
insert a s \ t ⊆ insert a (s \ t)

Alias of Set.insert_sdiff_subset.

source
theorem Set.insert_erase_invOn {α : Type u_1} {a : α} :
InvOn (insert a) (fun (s : Set α) => s \ {a}) {s : Set α | a ∈ s} {s : Set α | ¬a ∈ s}
source
@[simp]
theorem Set.sdiff_singleton_eq_self {α : Type u_1} {s : Set α} {a : α} (h : ¬a ∈ s) :
s \ {a} = s
source
@[deprecated Set.sdiff_singleton_eq_self (since := "2026-06-03")]
theorem Set.diff_singleton_eq_self {α : Type u_1} {s : Set α} {a : α} (h : ¬a ∈ s) :
s \ {a} = s

Alias of Set.sdiff_singleton_eq_self.

source
theorem Set.sdiff_singleton_ssubset {α : Type u_1} {s : Set α} {a : α} :
s \ {a} ⊂ s ↔ a ∈ s
source
@[deprecated Set.sdiff_singleton_ssubset (since := "2026-06-03")]
theorem Set.diff_singleton_ssubset {α : Type u_1} {s : Set α} {a : α} :
s \ {a} ⊂ s ↔ a ∈ s

Alias of Set.sdiff_singleton_ssubset.

source
@[simp]
theorem Set.insert_sdiff_singleton {α : Type u_1} {s : Set α} {a : α} :
insert a (s \ {a}) = insert a s
source
@[deprecated Set.insert_sdiff_singleton (since := "2026-06-03")]
theorem Set.insert_diff_singleton {α : Type u_1} {s : Set α} {a : α} :
insert a (s \ {a}) = insert a s

Alias of Set.insert_sdiff_singleton.

source
theorem Set.insert_sdiff_singleton_comm {α : Type u_1} {a b : α} (hab : a ≠ b) (s : Set α) :
insert a (s \ {b}) = insert a s \ {b}
source
@[deprecated Set.insert_sdiff_singleton_comm (since := "2026-06-03")]
theorem Set.insert_diff_singleton_comm {α : Type u_1} {a b : α} (hab : a ≠ b) (s : Set α) :
insert a (s \ {b}) = insert a s \ {b}

Alias of Set.insert_sdiff_singleton_comm.

source
@[simp]
theorem Set.insert_sdiff_insert {α : Type u_1} {s t : Set α} {a : α} :
insert a (s \ insert a t) = insert a (s \ t)
source
@[deprecated Set.insert_sdiff_insert (since := "2026-06-03")]
theorem Set.insert_diff_insert {α : Type u_1} {s t : Set α} {a : α} :
insert a (s \ insert a t) = insert a (s \ t)

Alias of Set.insert_sdiff_insert.

source
theorem Set.mem_sdiff_singleton {α : Type u_1} {s : Set α} {a b : α} :
a ∈ s \ {b} ↔ a ∈ s ∧ a ≠ b
source
@[deprecated Set.mem_sdiff_singleton (since := "2026-06-03")]
theorem Set.mem_diff_singleton {α : Type u_1} {s : Set α} {a b : α} :
a ∈ s \ {b} ↔ a ∈ s ∧ a ≠ b

Alias of Set.mem_sdiff_singleton.

source
theorem Set.mem_sdiff_singleton_empty {α : Type u_1} {s : Set α} {t : Set (Set α)} :
s ∈ t \ {∅} ↔ s ∈ t ∧ s.Nonempty
source
@[deprecated Set.mem_sdiff_singleton_empty (since := "2026-06-03")]
theorem Set.mem_diff_singleton_empty {α : Type u_1} {s : Set α} {t : Set (Set α)} :
s ∈ t \ {∅} ↔ s ∈ t ∧ s.Nonempty

Alias of Set.mem_sdiff_singleton_empty.

source
theorem Set.subset_insert_iff {α : Type u_1} {s t : Set α} {a : α} :
s ⊆ insert a t ↔ s ⊆ t ∨ a ∈ s ∧ s \ {a} ⊆ t
source
theorem Set.pair_sdiff_left {α : Type u_1} {a b : α} (hab : a ≠ b) :
{a, b} \ {a} = {b}
source
@[deprecated Set.pair_sdiff_left (since := "2026-06-03")]
theorem Set.pair_diff_left {α : Type u_1} {a b : α} (hab : a ≠ b) :
{a, b} \ {a} = {b}

Alias of Set.pair_sdiff_left.

source
theorem Set.pair_sdiff_right {α : Type u_1} {a b : α} (hab : a ≠ b) :
{a, b} \ {b} = {a}
source
@[deprecated Set.pair_sdiff_right (since := "2026-06-03")]
theorem Set.pair_diff_right {α : Type u_1} {a b : α} (hab : a ≠ b) :
{a, b} \ {b} = {a}

Alias of Set.pair_sdiff_right.

If-then-else for sets #

source
def Set.ite {α : Type u_1} (t s s' : Set α) :
Set α

ite for sets: Set.ite t s s' ∩ t = s ∩ t, Set.ite t s s' ∩ tᶜ = s' ∩ tᶜ. Defined as s ∩ t ∪ s' \ t.

Equations
Instances For
    source
    @[simp]
    theorem Set.ite_inter_self {α : Type u_1} (t s s' : Set α) :
    t.ite s s' ∩ t = s ∩ t
    source
    @[simp]
    theorem Set.ite_compl {α : Type u_1} (t s s' : Set α) :
    tᶜ.ite s s' = t.ite s' s
    source
    @[simp]
    theorem Set.ite_inter_compl_self {α : Type u_1} (t s s' : Set α) :
    t.ite s s' ∩ tᶜ = s' ∩ tᶜ
    source
    @[simp]
    theorem Set.ite_sdiff_self {α : Type u_1} (t s s' : Set α) :
    t.ite s s' \ t = s' \ t
    source
    @[deprecated Set.ite_sdiff_self (since := "2026-06-03")]
    theorem Set.ite_diff_self {α : Type u_1} (t s s' : Set α) :
    t.ite s s' \ t = s' \ t

    Alias of Set.ite_sdiff_self.

    source
    @[simp]
    theorem Set.ite_same {α : Type u_1} (t s : Set α) :
    t.ite s s = s
    source
    @[simp]
    theorem Set.ite_left {α : Type u_1} (s t : Set α) :
    s.ite s t = s ∪ t
    source
    @[simp]
    theorem Set.ite_right {α : Type u_1} (s t : Set α) :
    s.ite t s = t ∩ s
    source
    @[simp]
    theorem Set.ite_empty {α : Type u_1} (s s' : Set α) :
    ∅.ite s s' = s'
    source
    @[simp]
    theorem Set.ite_univ {α : Type u_1} (s s' : Set α) :
    univ.ite s s' = s
    source
    @[simp]
    theorem Set.ite_empty_left {α : Type u_1} (t s : Set α) :
    t.ite ∅ s = s \ t
    source
    @[simp]
    theorem Set.ite_empty_right {α : Type u_1} (t s : Set α) :
    t.ite s ∅ = s ∩ t
    source
    theorem Set.ite_mono {α : Type u_1} (t : Set α) {s₁ s₁' s₂ s₂' : Set α} (h : s₁ ⊆ s₂) (h' : s₁' ⊆ s₂') :
    t.ite s₁ s₁' ⊆ t.ite s₂ s₂'
    source
    theorem Set.ite_subset_union {α : Type u_1} (t s s' : Set α) :
    t.ite s s' ⊆ s ∪ s'
    source
    theorem Set.inter_subset_ite {α : Type u_1} (t s s' : Set α) :
    s ∩ s' ⊆ t.ite s s'
    source
    theorem Set.ite_inter_inter {α : Type u_1} (t s₁ s₂ s₁' s₂' : Set α) :
    t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') = t.ite s₁ s₁' ∩ t.ite s₂ s₂'
    source
    theorem Set.ite_inter {α : Type u_1} (t s₁ s₂ s : Set α) :
    t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s
    source
    theorem Set.ite_inter_of_inter_eq {α : Type u_1} (t : Set α) {s₁ s₂ s : Set α} (h : s₁ ∩ s = s₂ ∩ s) :
    t.ite s₁ s₂ ∩ s = s₁ ∩ s
    source
    theorem Set.subset_ite {α : Type u_1} {t s s' u : Set α} :
    u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s'
    source
    theorem Set.ite_eq_of_subset_left {α : Type u_1} (t : Set α) {s₁ s₂ : Set α} (h : s₁ ⊆ s₂) :
    t.ite s₁ s₂ = s₁ ∪ s₂ \ t
    source
    theorem Set.ite_eq_of_subset_right {α : Type u_1} (t : Set α) {s₁ s₂ : Set α} (h : s₂ ⊆ s₁) :
    t.ite s₁ s₂ = s₁ ∩ t ∪ s₂