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

@[implicit_reducible]

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

@[implicit_reducible]

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

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.

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.

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

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

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.

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

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

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

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

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_setOf {α : Type u_3} (p : α → Prop) : {a : α | p a}ᶜ = {a : α | ¬p a}

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ᶜ

@[simp]

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.

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.

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_diff_of_mem {α : Type u_1} {s t : Set α} {x : α} (hx : x ∈ t) : x ∉ s \ t

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[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.diff_subset_diff {α : Type u_1} {s₁ s₂ t₁ t₂ : Set α} : s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[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_diff {α : Type u_1} {s t u : Set α} : s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u

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.diff_ssubset_left_iff {α : Type u_1} {s t : Set α} : s \ t ⊂ s ↔ (s ∩ t).Nonempty

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

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

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

theorem Set.subset_diff_singleton {α : Type u_1} {s t : Set α} {a : α} (h : s ⊆ t) (ha : a ∉ s) : s ⊆ t \ {a}

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

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

@[simp]

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

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)

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

@[simp]

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

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

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.diff_singleton_eq_self {α : Type u_1} {s : Set α} {a : α} (h : a ∉ s) : s \ {a} = s

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

@[simp]

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

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

@[simp]

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

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

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

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_diff_left {α : Type u_1} {a b : α} (hab : a ≠ b) : {a, b} \ {a} = {b}

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

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.

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

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