Common.Set.Basic

Additional theorems and definitions useful in the context of Sets.

Minkowski Sum

def Set.minkowskiSum {α : Type u} [Add α] (s : Set α) (t : Set α) : Set α

Equations

• Set.minkowskiSum s t = {x : α | ∃ a ∈ s, ∃ b ∈ t, x = a + b}

theorem Set.nonempty_minkowski_sum_iff_nonempty_add_nonempty {α : Type u} [Add α] {s : Set α} {t : Set α} : Set.Nonempty (Set.minkowskiSum s t) ↔ Set.Nonempty s ∧ Set.Nonempty t

The sum of two Sets is nonempty iff the summands are nonempty.

Pair Sets

theorem Set.pair_eq_singleton_mem_imp_eq_self {α : Type u_1} {x : α} {y : α} (h : {x, y} = {x}) : y = x

If {x, y} = {x} then x = y.

theorem Set.pair_eq_singleton_mem_imp_eq_all {α : Type u_1} {x : α} {y : α} {z : α} (h : {x, y} = {z}) : x = z ∧ y = z

If {x, y} = {z} then x = y = z.

Subsets

theorem Set.ssubset_empty_iff_false {α : Type u_1} (S : Set α) : S ⊂ ∅ ↔ False

There exists no proper subset of ∅.

theorem Set.left_subset_union_eq_self {α : Type u_1} {A : Set α} {B : Set α} (h : A ⊆ B) : A ∪ B = B

If Set A is a subset of Set B, then A ∪ B = B.

theorem Set.right_subset_union_eq_self {α : Type u_1} {A : Set α} {B : Set α} (h : B ⊆ A) : A ∪ B = A

If Set B is a subset of Set A, then A ∪ B = B.

theorem Set.mem_mem_imp_pair_subset {α : Type u_1} {A : Set α} {x : α} {y : α} (hx : x ∈ A) (hy : y ∈ A) : {x, y} ⊆ A

If x and y are members of Set A, it follows {x, y} is a subset of A.

Powerset

theorem Set.self_mem_powerset_self {α : Type u_1} {A : Set α} : A ∈ 𝒫 A

Every Set is a member of its own powerset.

Cartesian Product

theorem Set.prod_left_emptyset_eq_emptyset {α : Type u_1} {β : Type u_2} {A : Set α} : Set.prod ∅ A = ∅

For any Set A, ∅ × A = ∅.

theorem Set.prod_right_emptyset_eq_emptyset {α : Type u_1} {β : Type u_2} {A : Set α} : Set.prod A ∅ = ∅

For any Set A, A × ∅ = ∅.

theorem Set.prod_nonempty_nonempty_imp_nonempty_prod {α : Type u_1} {β : Type u_2} {A : Set α} {B : Set β} : A ≠ ∅ ∧ B ≠ ∅ ↔ Set.prod A B ≠ ∅

For any Sets A and B, if both A and B are nonempty, then A × B is also nonempty.

Difference

theorem Set.diff_ssubset_diff_left {α : Type u_1} {x : α} {A : Set α} {B : Set α} (h : A ⊂ B) : x ∈ A → A \ {x} ⊂ B \ {x}

For any sets A ⊂ B, if x ∈ A then A - {x} ⊂ B - {x}.

theorem Set.diff_ssubset_nonempty {α : Type u_1} {A : Set α} {B : Set α} (h : A ⊂ B) : Set.Nonempty (B \ A)

For any sets A ⊂ B, B \ A is nonempty.

theorem Set.not_mem_diff_eq_self {α : Type u_1} {a : α} {A : Set α} (h : a ∉ A) : A \ {a} = A

If an element x is not a member of a set A, then A - {x} = A.

theorem Set.diff_mem_diff_mem_eq_diff_diff_mem {α : Type u_1} {A : Set α} {B : Set α} {a : α} : (A \ {a}) \ (B \ {a}) = (A \ B) \ {a}

Given two sets A and B, (A - {a}) - (B - {b}) = (A - B) - {a}.

theorem Set.univ_diff_self_eq_compl {α : Type u_1} (A : Set α) : Set.univ \ A = Set.compl A

For any set A, the difference between the sample space and A is the complement of A.

theorem Set.univ_diff_compl_eq_self {α : Type u_1} (A : Set α) : Set.univ \ Set.compl A = A

For any set A, the difference between the sample space and the complement of A is A.

Symmetric Difference

theorem Set.symm_diff_mem_left {α : Type u_1} {x : α} {A : Set α} {B : Set α} (hA : x ∈ A) (hB : x ∉ B) : x ∈ A ∆ B

If x ∈ A and x ∉ B, then x ∈ A ∆ B.

theorem Set.symm_diff_mem_right {α : Type u_1} {x : α} {A : Set α} {B : Set α} (hA : x ∉ A) (hB : x ∈ B) : x ∈ A ∆ B

If x ∉ A and x ∈ B, then x ∈ A ∆ B.

theorem Set.symm_diff_mem_both_not_mem {α : Type u_1} {x : α} {A : Set α} {B : Set α} (hA : x ∈ A) (hB : x ∈ B) : x ∉ A ∆ B

If x ∈ A and x ∈ B, then x ∉ A ∆ B.

theorem Set.symm_diff_not_mem_both_not_mem {α : Type u_1} {x : α} {A : Set α} {B : Set α} (nA : x ∉ A) (nB : x ∉ B) : x ∉ A ∆ B

If x ∉ A and x ∉ B, then x ∉ A ∆ B.

theorem Set.mem_symm_diff_iff_exclusive_mem {α : Type u_1} {x : α} {A : Set α} {B : Set α} : x ∈ A ∆ B ↔ x ∈ A ∧ x ∉ B ∨ x ∉ A ∧ x ∈ B

x is a member of the symmDiff of A and B iff x ∈ A ∧ x ∉ B or x ∉ A ∧ x ∈ B.

theorem Set.not_mem_symm_diff_inter_or_not_union {α : Type u_1} {x : α} {A : Set α} {B : Set α} : x ∉ A ∆ B ↔ x ∈ A ∩ B ∨ x ∉ A ∪ B

x is not a member of the symmDiff of A and B iff x ∈ A ∩ B or x ∉ A ∪ B.

This is the contraposition of mem_symm_diff_iff_exclusive_mem.