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
instance Set.instBooleanAlgebra {α : Type u_1} :
BooleanAlgebra (Set α)
Equations
  • One or more equations did not get rendered due to their size.
source
theorem Set.inter_diff_assoc {α : Type u_1} (a b c : Set α) :
(a ∩ b) \ c = a ∩ (b \ c)

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_diff_assoc.

source
theorem Set.inter_sdiff_left_comm {α : Type u_1} (s t u : Set α) :
s ∩ (t \ u) = t ∩ (s \ u)
source
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
source
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

A version of diff_union_diff_cancel with more general hypotheses.

source
theorem Set.diff_diff_eq_sdiff_union {α : Type u_1} {s t u : Set α} (h : u ⊆ s) :
s \ (t \ u) = s \ t ∪ u
source
theorem Set.inter_diff_distrib_left {α : Type u_1} (s t u : Set α) :
s ∩ (t \ u) = (s ∩ t) \ (s ∩ u)
source
theorem Set.inter_diff_distrib_right {α : Type u_1} (s t u : Set α) :
s \ t ∩ u = (s ∩ u) \ (t ∩ u)
source
theorem Set.diff_inter_distrib_right {α : Type u_1} (s t r : Set α) :
(t ∩ r) \ s = t \ s ∩ (r \ s)

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
@[deprecated Set.notMem_of_mem_compl (since := "2025-05-23")]
theorem Set.not_mem_of_mem_compl {α : Type u_1} {s : Set α} {x : α} (h : x ∈ sᶜ) :
x ∉ s

Alias of Set.notMem_of_mem_compl.

source
theorem Set.notMem_compl_iff {α : Type u_1} {s : Set α} {x : α} :
x ∉ sᶜ ↔ x ∈ s
source
@[deprecated Set.notMem_compl_iff (since := "2025-05-23")]
theorem Set.not_mem_compl_iff {α : Type u_1} {s : Set α} {x : α} :
x ∉ sᶜ ↔ x ∈ s

Alias of Set.notMem_compl_iff.

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

Lemmas about set difference #

source
theorem Set.notMem_diff_of_mem {α : Type u_1} {s t : Set α} {x : α} (hx : x ∈ t) :
x ∉ s \ t
source
@[deprecated Set.notMem_diff_of_mem (since := "2025-05-23")]
theorem Set.not_mem_diff_of_mem {α : Type u_1} {s t : Set α} {x : α} (hx : x ∈ t) :
x ∉ s \ t

Alias of Set.notMem_diff_of_mem.

source
theorem Set.mem_of_mem_diff {α : Type u_1} {s t : Set α} {x : α} (h : x ∈ s \ t) :
x ∈ s
source
theorem Set.notMem_of_mem_diff {α : Type u_1} {s t : Set α} {x : α} (h : x ∈ s \ t) :
x ∉ t
source
@[deprecated Set.notMem_of_mem_diff (since := "2025-05-23")]
theorem Set.not_mem_of_mem_diff {α : Type u_1} {s t : Set α} {x : α} (h : x ∈ s \ t) :
x ∉ t

Alias of Set.notMem_of_mem_diff.

source
theorem Set.diff_eq_compl_inter {α : Type u_1} {s t : Set α} :
s \ t = tᶜ ∩ s
source
theorem Set.diff_nonempty {α : Type u_1} {s t : Set α} :
(s \ t).Nonempty ↔ ¬s ⊆ t
source
theorem Set.diff_subset {α : Type u_1} {s t : Set α} :
s \ t ⊆ s
source
theorem Set.diff_subset_compl {α : Type u_1} (s t : Set α) :
s \ t ⊆ tᶜ
source
theorem Set.union_diff_cancel' {α : Type u_1} {s t u : Set α} (h₁ : s ⊆ t) (h₂ : t ⊆ u) :
t ∪ u \ s = u
source
theorem Set.union_diff_cancel {α : Type u_1} {s t : Set α} (h : s ⊆ t) :
s ∪ t \ s = t
source
theorem Set.union_diff_cancel_left {α : Type u_1} {s t : Set α} (h : s ∩ t ⊆ ∅) :
(s ∪ t) \ s = t
source
theorem Set.union_diff_cancel_right {α : Type u_1} {s t : Set α} (h : s ∩ t ⊆ ∅) :
(s ∪ t) \ t = s
source
@[simp]
theorem Set.union_diff_left {α : Type u_1} {s t : Set α} :
(s ∪ t) \ s = t \ s
source
@[simp]
theorem Set.union_diff_right {α : Type u_1} {s t : Set α} :
(s ∪ t) \ t = s \ t
source
theorem Set.union_diff_distrib {α : Type u_1} {s t u : Set α} :
(s ∪ t) \ u = s \ u ∪ t \ u
source
@[simp]
theorem Set.inter_diff_self {α : Type u_1} (a b : Set α) :
a ∩ (b \ a) = ∅
source
@[simp]
theorem Set.inter_union_diff {α : Type u_1} (s t : Set α) :
s ∩ t ∪ s \ t = s
source
@[simp]
theorem Set.diff_union_inter {α : Type u_1} (s t : Set α) :
s \ t ∪ s ∩ t = s
source
@[simp]
theorem Set.inter_union_compl {α : Type u_1} (s t : Set α) :
s ∩ t ∪ s ∩ tᶜ = s
source
theorem Set.diff_subset_diff {α : Type u_1} {s₁ s₂ t₁ t₂ : Set α} :
s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂
source
theorem Set.diff_subset_diff_left {α : Type u_1} {s₁ s₂ t : Set α} (h : s₁ ⊆ s₂) :
s₁ \ t ⊆ s₂ \ t
source
theorem Set.diff_subset_diff_right {α : Type u_1} {s t u : Set α} (h : t ⊆ u) :
s \ u ⊆ s \ t
source
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
source
theorem Set.compl_eq_univ_diff {α : Type u_1} (s : Set α) :
sᶜ = univ \ s
source
@[simp]
theorem Set.empty_diff {α : Type u_1} (s : Set α) :
∅ \ s = ∅
source
theorem Set.diff_eq_empty {α : Type u_1} {s t : Set α} :
s \ t = ∅ ↔ s ⊆ t
source
@[simp]
theorem Set.diff_empty {α : Type u_1} {s : Set α} :
s \ ∅ = s
source
@[simp]
theorem Set.diff_univ {α : Type u_1} (s : Set α) :
s \ univ = ∅
source
theorem Set.diff_diff {α : Type u_1} {s t u : Set α} :
(s \ t) \ u = s \ (t ∪ u)
source
theorem Set.diff_diff_comm {α : Type u_1} {s t u : Set α} :
(s \ t) \ u = (s \ u) \ t
source
theorem Set.diff_subset_iff {α : Type u_1} {s t u : Set α} :
s \ t ⊆ u ↔ s ⊆ t ∪ u
source
theorem Set.subset_diff_union {α : Type u_1} (s t : Set α) :
s ⊆ s \ t ∪ t
source
theorem Set.diff_union_of_subset {α : Type u_1} {s t : Set α} (h : t ⊆ s) :
s \ t ∪ t = s
source
theorem Set.diff_subset_comm {α : Type u_1} {s t u : Set α} :
s \ t ⊆ u ↔ s \ u ⊆ t
source
theorem Set.diff_inter {α : Type u_1} {s t u : Set α} :
s \ (t ∩ u) = s \ t ∪ s \ u
source
theorem Set.diff_inter_diff {α : Type u_1} {s t u : Set α} :
s \ t ∩ (s \ u) = s \ (t ∪ u)
source
theorem Set.diff_compl {α : Type u_1} {s t : Set α} :
s \ tᶜ = s ∩ t
source
theorem Set.compl_diff {α : Type u_1} {s t : Set α} :
(t \ s)ᶜ = s ∪ tᶜ
source
theorem Set.diff_diff_right {α : Type u_1} {s t u : Set α} :
s \ (t \ u) = s \ t ∪ s ∩ u
source
theorem Set.inter_diff_right_comm {α : Type u_1} {s t u : Set α} :
(s ∩ t) \ u = s \ u ∩ t
source
theorem Set.diff_inter_right_comm {α : Type u_1} {s t u : Set α} :
s \ u ∩ t = (s ∩ t) \ u
source
@[simp]
theorem Set.union_diff_self {α : Type u_1} {s t : Set α} :
s ∪ t \ s = s ∪ t
source
@[simp]
theorem Set.diff_union_self {α : Type u_1} {s t : Set α} :
s \ t ∪ t = s ∪ t
source
@[simp]
theorem Set.diff_inter_self {α : Type u_1} {a b : Set α} :
b \ a ∩ a = ∅
source
@[simp]
theorem Set.diff_inter_self_eq_diff {α : Type u_1} {s t : Set α} :
s \ (t ∩ s) = s \ t
source
@[simp]
theorem Set.diff_self_inter {α : Type u_1} {s t : Set α} :
s \ (s ∩ t) = s \ t
source
theorem Set.diff_self {α : Type u_1} {s : Set α} :
s \ s = ∅
source
theorem Set.diff_diff_right_self {α : Type u_1} (s t : Set α) :
s \ (s \ t) = s ∩ t
source
theorem Set.diff_diff_cancel_left {α : Type u_1} {s t : Set α} (h : s ⊆ t) :
t \ (t \ s) = s
source
theorem Set.union_eq_diff_union_diff_union_inter {α : Type u_1} (s t : Set α) :
s ∪ t = s \ t ∪ t \ s ∪ s ∩ t
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}

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_diff_self {α : Type u_1} (t s s' : Set α) :
    t.ite s s' \ t = s' \ t
    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₂