Boolean algebra of sets

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

Notation

• sᶜ for the complement of s

Tags

set, sets, subset, subsets, complement

@[instance_reducible]

instance Set.instHImp {α : Type u_1} : HImp (Set α)

Equations

• Set.instHImp = { himp := fun (s t : Set α) => {x : α | x ∈ s → x ∈ t} }

@[simp]

theorem Set.mem_himp_iff {α : Type u_1} {s t : Set α} {a : α} : a ∈ s ⇨ t ↔ a ∈ s → a ∈ t

@[instance_reducible]

instance Set.instBooleanAlgebra {α : Type u_1} : BooleanAlgebra (Set α)

Equations

• One or more equations did not get rendered due to their size.

theorem Set.himp_def {α : Type u_1} {s t : Set α} : s ⇨ t = t ∪ sᶜ

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.

@[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.

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.

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

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

@[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.

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.

@[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.

theorem Set.sdiff_sdiff_eq_sdiff_union {α : Type u_1} {s t u : Set α} (h : u ⊆ s) : s \ (t \ u) = s \ t ∪ u

@[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.

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

@[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.

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

@[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.

theorem Set.sdiff_inter_distrib_right {α : Type u_1} (s t r : Set α) : (t ∩ r) \ s = t \ s ∩ (r \ s)

@[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

theorem Set.compl_def {α : Type u_1} (s : Set α) : sᶜ = {x : α | ¬x ∈ s}

theorem Set.mem_compl {α : Type u_1} {s : Set α} {x : α} (h : ¬x ∈ s) : x ∈ sᶜ

theorem Set.compl_ofPred {α : Type u_3} (p : α → Prop) : {a : α | p a}ᶜ = {a : α | ¬p a}

@[deprecated Set.compl_ofPred (since := "2026-07-09")]

theorem Set.compl_setOf {α : Type u_3} (p : α → Prop) : {a : α | p a}ᶜ = {a : α | ¬p a}

Alias of Set.compl_ofPred.

theorem Set.notMem_of_mem_compl {α : Type u_1} {s : Set α} {x : α} (h : x ∈ sᶜ) : ¬x ∈ s

theorem Set.notMem_compl_iff {α : Type u_1} {s : Set α} {x : α} : ¬x ∈ sᶜ ↔ x ∈ s

@[simp]

theorem Set.inter_compl_self {α : Type u_1} (s : Set α) : s ∩ sᶜ = ∅

@[simp]

theorem Set.compl_inter_self {α : Type u_1} (s : Set α) : sᶜ ∩ s = ∅

@[simp]

theorem Set.compl_empty {α : Type u_1} : ∅ᶜ = univ

@[simp]

theorem Set.compl_union {α : Type u_1} (s t : Set α) : (s ∪ t)ᶜ = sᶜ ∩ tᶜ

theorem Set.compl_inter {α : Type u_1} (s t : Set α) : (s ∩ t)ᶜ = sᶜ ∪ tᶜ

@[simp]

theorem Set.compl_univ {α : Type u_1} : univᶜ = ∅

@[simp]

theorem Set.compl_empty_iff {α : Type u_1} {s : Set α} : sᶜ = ∅ ↔ s = univ

@[simp]

theorem Set.compl_univ_iff {α : Type u_1} {s : Set α} : sᶜ = univ ↔ s = ∅

theorem Set.compl_ne_univ {α : Type u_1} {s : Set α} : sᶜ ≠ univ ↔ s.Nonempty

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)ᶜ

theorem Set.nonempty_compl {α : Type u_1} {s : Set α} : sᶜ.Nonempty ↔ s ≠ univ

theorem Set.union_eq_compl_compl_inter_compl {α : Type u_1} (s t : Set α) : s ∪ t = (sᶜ ∩ tᶜ)ᶜ

theorem Set.inter_eq_compl_compl_union_compl {α : Type u_1} (s t : Set α) : s ∩ t = (sᶜ ∪ tᶜ)ᶜ

@[simp]

theorem Set.union_compl_self {α : Type u_1} (s : Set α) : s ∪ sᶜ = univ

@[simp]

theorem Set.compl_union_self {α : Type u_1} (s : Set α) : sᶜ ∪ s = univ

theorem Set.compl_subset_comm {α : Type u_1} {s t : Set α} : sᶜ ⊆ t ↔ tᶜ ⊆ s

theorem Set.subset_compl_comm {α : Type u_1} {s t : Set α} : s ⊆ tᶜ ↔ t ⊆ sᶜ

theorem Set.compl_subset_compl {α : Type u_1} {s t : Set α} : sᶜ ⊆ tᶜ ↔ t ⊆ s

theorem Set.compl_subset_compl_of_subset {α : Type u_1} {s t : Set α} (h : t ⊆ s) : sᶜ ⊆ tᶜ

theorem Set.subset_union_compl_iff_inter_subset {α : Type u_1} {s t u : Set α} : s ⊆ t ∪ uᶜ ↔ s ∩ u ⊆ t

theorem Set.compl_subset_iff_union {α : Type u_1} {s t : Set α} : sᶜ ⊆ t ↔ s ∪ t = univ

theorem Set.inter_subset {α : Type u_1} (a b c : Set α) : a ∩ b ⊆ c ↔ a ⊆ bᶜ ∪ c

theorem Set.inter_compl_nonempty_iff {α : Type u_1} {s t : Set α} : (s ∩ tᶜ).Nonempty ↔ ¬s ⊆ t

theorem Set.subset_compl_iff_disjoint_left {α : Type u_1} {s t : Set α} : s ⊆ tᶜ ↔ Disjoint t s

theorem Set.subset_compl_iff_disjoint_right {α : Type u_1} {s t : Set α} : s ⊆ tᶜ ↔ Disjoint s t

theorem Set.disjoint_compl_left_iff_subset {α : Type u_1} {s t : Set α} : Disjoint sᶜ t ↔ t ⊆ s

theorem Set.disjoint_compl_right_iff_subset {α : Type u_1} {s t : Set α} : Disjoint s tᶜ ↔ s ⊆ t

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.

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.

@[deprecated LE.le.disjoint_compl_left (since := "2026-06-05")]

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.

@[deprecated LE.le.disjoint_compl_right (since := "2026-06-05")]

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.

@[simp]

theorem Set.nonempty_compl_of_nontrivial {α : Type u_1} [Nontrivial α] (x : α) : {x}ᶜ.Nonempty

theorem Set.mem_compl_singleton_iff {α : Type u_1} {a b : α} : a ∈ {b}ᶜ ↔ a ≠ b

theorem Set.compl_singleton_eq {α : Type u_1} (a : α) : {a}ᶜ = {x : α | x ≠ a}

@[simp]

theorem Set.compl_ne_eq_singleton {α : Type u_1} (a : α) : {x : α | x ≠ a}ᶜ = {a}

@[simp]

theorem Set.subset_compl_singleton_iff {α : Type u_1} {s : Set α} {a : α} : s ⊆ {a}ᶜ ↔ ¬a ∈ s

Lemmas about set difference

theorem Set.notMem_sdiff_of_mem {α : Type u_1} {s t : Set α} {x : α} (hx : x ∈ t) : ¬x ∈ s \ t

@[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.

theorem Set.mem_of_mem_sdiff {α : Type u_1} {s t : Set α} {x : α} (h : x ∈ s \ t) : x ∈ s

@[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.

theorem Set.notMem_of_mem_sdiff {α : Type u_1} {s t : Set α} {x : α} (h : x ∈ s \ t) : ¬x ∈ t

@[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.

theorem Set.sdiff_eq_compl_inter {α : Type u_1} {s t : Set α} : s \ t = tᶜ ∩ s

@[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.

theorem Set.sdiff_nonempty {α : Type u_1} {s t : Set α} : (s \ t).Nonempty ↔ ¬s ⊆ t

@[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.

theorem Set.sdiff_subset {α : Type u_1} {s t : Set α} : s \ t ⊆ s

@[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.

theorem Set.sdiff_subset_compl {α : Type u_1} (s t : Set α) : s \ t ⊆ tᶜ

@[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.

theorem Set.union_sdiff_cancel' {α : Type u_1} {s t u : Set α} (h₁ : s ⊆ t) (h₂ : t ⊆ u) : t ∪ u \ s = u

@[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'.

theorem Set.union_sdiff_cancel {α : Type u_1} {s t : Set α} (h : s ⊆ t) : s ∪ t \ s = t

@[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.

theorem Set.union_sdiff_cancel_left {α : Type u_1} {s t : Set α} (h : s ∩ t ⊆ ∅) : (s ∪ t) \ s = t

@[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.

theorem Set.union_sdiff_cancel_right {α : Type u_1} {s t : Set α} (h : s ∩ t ⊆ ∅) : (s ∪ t) \ t = s

@[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.

@[simp]

theorem Set.union_sdiff_left {α : Type u_1} {s t : Set α} : (s ∪ t) \ s = t \ s

@[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.

@[simp]

theorem Set.union_sdiff_right {α : Type u_1} {s t : Set α} : (s ∪ t) \ t = s \ t

@[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.

theorem Set.union_sdiff_distrib {α : Type u_1} {s t u : Set α} : (s ∪ t) \ u = s \ u ∪ t \ u

@[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.

@[simp]

theorem Set.inter_sdiff_self {α : Type u_1} (a b : Set α) : a ∩ (b \ a) = ∅

@[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.

@[simp]

theorem Set.inter_union_sdiff {α : Type u_1} (s t : Set α) : s ∩ t ∪ s \ t = s

@[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.

@[simp]

theorem Set.sdiff_union_inter {α : Type u_1} (s t : Set α) : s \ t ∪ s ∩ t = s

@[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.

@[simp]

theorem Set.inter_union_compl {α : Type u_1} (s t : Set α) : s ∩ t ∪ s ∩ tᶜ = s

theorem Set.subset_inter_union_compl_left {α : Type u_1} (s t : Set α) : t ⊆ s ∩ t ∪ sᶜ

theorem Set.subset_inter_union_compl_right {α : Type u_1} (s t : Set α) : s ⊆ s ∩ t ∪ tᶜ

theorem Set.union_inter_compl_left_subset {α : Type u_1} (s t : Set α) : (s ∪ t) ∩ sᶜ ⊆ t

theorem Set.union_inter_compl_right_subset {α : Type u_1} (s t : Set α) : (s ∪ t) ∩ tᶜ ⊆ s

theorem Set.sdiff_subset_sdiff {α : Type u_1} {s₁ s₂ t₁ t₂ : Set α} : s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂

@[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.

theorem Set.sdiff_subset_sdiff_left {α : Type u_1} {s₁ s₂ t : Set α} (h : s₁ ⊆ s₂) : s₁ \ t ⊆ s₂ \ t

@[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.

theorem Set.sdiff_subset_sdiff_right {α : Type u_1} {s t u : Set α} (h : t ⊆ u) : s \ u ⊆ s \ t

@[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.

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

@[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.

theorem Set.compl_eq_univ_sdiff {α : Type u_1} (s : Set α) : sᶜ = univ \ s

@[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.

@[simp]

theorem Set.empty_sdiff {α : Type u_1} (s : Set α) : ∅ \ s = ∅

@[deprecated Set.empty_sdiff (since := "2026-06-03")]

theorem Set.empty_diff {α : Type u_1} (s : Set α) : ∅ \ s = ∅

Alias of Set.empty_sdiff.

theorem Set.sdiff_eq_empty {α : Type u_1} {s t : Set α} : s \ t = ∅ ↔ s ⊆ t

@[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.

@[simp]

theorem Set.sdiff_empty {α : Type u_1} {s : Set α} : s \ ∅ = s

@[deprecated Set.sdiff_empty (since := "2026-06-03")]

theorem Set.diff_empty {α : Type u_1} {s : Set α} : s \ ∅ = s

Alias of Set.sdiff_empty.

@[simp]

theorem Set.sdiff_univ {α : Type u_1} (s : Set α) : s \ univ = ∅

@[deprecated Set.sdiff_univ (since := "2026-06-03")]

theorem Set.diff_univ {α : Type u_1} (s : Set α) : s \ univ = ∅

Alias of Set.sdiff_univ.

theorem Set.sdiff_sdiff {α : Type u_1} {s t u : Set α} : (s \ t) \ u = s \ (t ∪ u)

@[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.

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

@[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.

@[simp]

theorem Set.sdiff_subset_iff {α : Type u_1} {s t u : Set α} : s \ t ⊆ u ↔ s ⊆ t ∪ u

@[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.

theorem Set.subset_sdiff_union {α : Type u_1} (s t : Set α) : s ⊆ s \ t ∪ t

@[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.

theorem Set.sdiff_union_of_subset {α : Type u_1} {s t : Set α} (h : t ⊆ s) : s \ t ∪ t = s

@[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.

theorem Set.sdiff_subset_comm {α : Type u_1} {s t u : Set α} : s \ t ⊆ u ↔ s \ u ⊆ t

@[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.

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

@[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.

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

@[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.

theorem Set.sdiff_compl {α : Type u_1} {s t : Set α} : s \ tᶜ = s ∩ t

@[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.

theorem Set.compl_sdiff {α : Type u_1} {s t : Set α} : (t \ s)ᶜ = s ∪ tᶜ

@[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.

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

@[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.

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

@[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.

@[simp]

theorem Set.union_sdiff_self {α : Type u_1} {s t : Set α} : s ∪ t \ s = s ∪ t

@[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.

@[simp]

theorem Set.sdiff_union_self {α : Type u_1} {s t : Set α} : s \ t ∪ t = s ∪ t

@[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.

@[simp]

theorem Set.sdiff_inter_self {α : Type u_1} {a b : Set α} : b \ a ∩ a = ∅

@[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.

@[simp]

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

@[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.

@[simp]

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

@[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.

theorem Set.sdiff_self {α : Type u_1} {s : Set α} : s \ s = ∅

@[deprecated Set.sdiff_self (since := "2026-06-03")]

theorem Set.diff_self {α : Type u_1} {s : Set α} : s \ s = ∅

Alias of Set.sdiff_self.

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

@[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.

theorem Set.sdiff_sdiff_cancel_left {α : Type u_1} {s t : Set α} (h : s ⊆ t) : t \ (t \ s) = s

@[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.

theorem Set.union_eq_sdiff_union_sdiff_union_inter {α : Type u_1} (s t : Set α) : s ∪ t = s \ t ∪ t \ s ∪ s ∩ t

@[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.

@[simp]

theorem Set.sdiff_sep_self {α : Type u_1} (s : Set α) (p : α → Prop) : s \ {a : α | a ∈ s ∧ p a} = {a : α | a ∈ s ∧ ¬p a}

theorem Set.disjoint_sdiff_left {α : Type u_1} {s t : Set α} : Disjoint (t \ s) s

theorem Set.disjoint_sdiff_right {α : Type u_1} {s t : Set α} : Disjoint s (t \ s)

theorem Set.disjoint_sdiff_inter {α : Type u_1} {s t : Set α} : Disjoint (s \ t) (s ∩ t)

theorem Set.subset_sdiff {α : Type u_1} {s t u : Set α} : s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u

@[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.

theorem Set.disjoint_of_subset_iff_left_eq_empty {α : Type u_1} {s t : Set α} (h : s ⊆ t) : Disjoint s t ↔ s = ∅

@[simp]

theorem Set.sdiff_ssubset_left_iff {α : Type u_1} {s t : Set α} : s \ t ⊂ s ↔ (s ∩ t).Nonempty

@[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.

theorem LE.le.sdiff_ssubset_of_nonempty {α : Type u_1} {s t : Set α} (hst : s ⊆ t) (hs : s.Nonempty) : t \ s ⊂ t

@[deprecated LE.le.sdiff_ssubset_of_nonempty (since := "2026-06-05")]

theorem HasSubset.Subset.sdiff_ssubset_of_nonempty {α : Type u_1} {s t : Set α} (hst : s ⊆ t) (hs : s.Nonempty) : t \ s ⊂ t

Alias of LE.le.sdiff_ssubset_of_nonempty.

@[deprecated LE.le.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 LE.le.sdiff_ssubset_of_nonempty.

theorem Set.ssubset_iff_sdiff_singleton {α : Type u_1} {s t : Set α} : s ⊂ t ↔ ∃ (a : α), a ∈ t ∧ s ⊆ t \ {a}

theorem Set.sdiff_singleton_subset_iff {α : Type u_1} {s t : Set α} {a : α} : s \ {a} ⊆ t ↔ s ⊆ insert a t

@[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.

theorem Set.subset_sdiff_singleton {α : Type u_1} {s t : Set α} {a : α} (h : s ⊆ t) (ha : ¬a ∈ s) : s ⊆ t \ {a}

@[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.

theorem Set.subset_insert_sdiff_singleton {α : Type u_1} (x : α) (s : Set α) : s ⊆ insert x (s \ {x})

@[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.

theorem Set.sdiff_insert_of_notMem {α : Type u_1} {s t : Set α} {a : α} (h : ¬a ∈ s) : s \ insert a t = s \ t

@[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.

@[simp]

theorem Set.insert_sdiff_of_mem {α : Type u_1} {t : Set α} {a : α} (s : Set α) (h : a ∈ t) : insert a s \ t = s \ t

@[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.

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)

@[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.

theorem Set.insert_sdiff_self_of_notMem {α : Type u_1} {s : Set α} {a : α} (h : ¬a ∈ s) : insert a s \ {a} = s

@[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.

@[simp]

theorem Set.insert_sdiff_self_of_mem {α : Type u_1} {s : Set α} {a : α} (ha : a ∈ s) : insert a (s \ {a}) = s

@[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.

theorem Set.insert_sdiff_subset {α : Type u_1} {s t : Set α} {a : α} : insert a s \ t ⊆ insert a (s \ t)

@[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.

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}

@[simp]

theorem Set.sdiff_singleton_eq_self {α : Type u_1} {s : Set α} {a : α} (h : ¬a ∈ s) : s \ {a} = s

@[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.

theorem Set.sdiff_singleton_ssubset {α : Type u_1} {s : Set α} {a : α} : s \ {a} ⊂ s ↔ a ∈ s

@[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.

@[simp]

theorem Set.insert_sdiff_singleton {α : Type u_1} {s : Set α} {a : α} : insert a (s \ {a}) = insert a s

@[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.

theorem Set.insert_sdiff_singleton_comm {α : Type u_1} {a b : α} (hab : a ≠ b) (s : Set α) : insert a (s \ {b}) = insert a s \ {b}

@[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.

@[simp]

theorem Set.insert_sdiff_insert {α : Type u_1} {s t : Set α} {a : α} : insert a (s \ insert a t) = insert a (s \ t)

@[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.

theorem Set.mem_sdiff_singleton {α : Type u_1} {s : Set α} {a b : α} : a ∈ s \ {b} ↔ a ∈ s ∧ a ≠ b

@[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.

theorem Set.mem_sdiff_singleton_empty {α : Type u_1} {s : Set α} {t : Set (Set α)} : s ∈ t \ {∅} ↔ s ∈ t ∧ s.Nonempty

@[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.

theorem Set.subset_insert_iff {α : Type u_1} {s t : Set α} {a : α} : s ⊆ insert a t ↔ s ⊆ t ∨ a ∈ s ∧ s \ {a} ⊆ t

theorem Set.pair_sdiff_left {α : Type u_1} {a b : α} (hab : a ≠ b) : {a, b} \ {a} = {b}

@[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.

theorem Set.pair_sdiff_right {α : Type u_1} {a b : α} (hab : a ≠ b) : {a, b} \ {b} = {a}

@[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

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

• t.ite s s' = s ∩ t ∪ s' \ t

@[simp]

theorem Set.ite_inter_self {α : Type u_1} (t s s' : Set α) : t.ite s s' ∩ t = s ∩ t

@[simp]

theorem Set.ite_compl {α : Type u_1} (t s s' : Set α) : tᶜ.ite s s' = t.ite s' s

@[simp]

theorem Set.ite_inter_compl_self {α : Type u_1} (t s s' : Set α) : t.ite s s' ∩ tᶜ = s' ∩ tᶜ

@[simp]

theorem Set.ite_sdiff_self {α : Type u_1} (t s s' : Set α) : t.ite s s' \ t = s' \ t

@[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.

@[simp]

theorem Set.ite_same {α : Type u_1} (t s : Set α) : t.ite s s = s

@[simp]

theorem Set.ite_left {α : Type u_1} (s t : Set α) : s.ite s t = s ∪ t

@[simp]

theorem Set.ite_right {α : Type u_1} (s t : Set α) : s.ite t s = t ∩ s

@[simp]

theorem Set.ite_empty {α : Type u_1} (s s' : Set α) : ∅.ite s s' = s'

@[simp]

theorem Set.ite_univ {α : Type u_1} (s s' : Set α) : univ.ite s s' = s

@[simp]

theorem Set.ite_empty_left {α : Type u_1} (t s : Set α) : t.ite ∅ s = s \ t

@[simp]

theorem Set.ite_empty_right {α : Type u_1} (t s : Set α) : t.ite s ∅ = s ∩ t

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₂'

theorem Set.ite_subset_union {α : Type u_1} (t s s' : Set α) : t.ite s s' ⊆ s ∪ s'

theorem Set.inter_subset_ite {α : Type u_1} (t s s' : Set α) : s ∩ s' ⊆ t.ite s s'

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₂'

theorem Set.ite_inter {α : Type u_1} (t s₁ s₂ s : Set α) : t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s

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

theorem Set.subset_ite {α : Type u_1} {t s s' u : Set α} : u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s'

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

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₂