@[reducible, inline]

abbrev ElementCollection (α : Type u) : Type u

Definition 0.3.1: A set is a collection of objects called elements or members. A set with no objects is the empty set, written ∅ (or {}).

Equations

• ElementCollection α = Set α

@[reducible, inline]

abbrev emptyElementCollection (α : Type u) : ElementCollection α

The empty set from Definition 0.3.1 is mathlib's ∅.

Equations

• emptyElementCollection α = ∅

theorem elementCollection_eq_set (α : Type u) : ElementCollection α = Set α

The book's notion of set coincides with mathlib's Set.

@[reducible, inline]

abbrev subsetElementCollection {α : Type u} (A B : ElementCollection α) : Prop

Definition 0.3.2: (i) A ⊆ B means every x ∈ A also satisfies x ∈ B; (ii) A = B when each is a subset of the other (otherwise A ≠ B); (iii) A ⊂ B when A ⊆ B but A ≠ B.

Equations

• subsetElementCollection A B = (A ⊆ B)

theorem subsetElementCollection_iff {α : Type u} {A B : ElementCollection α} : subsetElementCollection A B ↔ A ⊆ B

The book's notion of subset is mathlib's ⊆.

theorem elementCollection_eq_iff_subset_subset {α : Type u} {A B : ElementCollection α} : A = B ↔ subsetElementCollection A B ∧ subsetElementCollection B A

The book's definition of equality of sets is mutual inclusion.

@[reducible, inline]

abbrev properSubsetElementCollection {α : Type u} (A B : ElementCollection α) : Prop

Book notion of a proper subset: contained but not equal.

Equations

• properSubsetElementCollection A B = (subsetElementCollection A B ∧ A ≠ B)

theorem properSubsetElementCollection_iff {α : Type u} {A B : ElementCollection α} : properSubsetElementCollection A B ↔ A ⊂ B

The book's notion of proper subset coincides with mathlib's strict subset ⊂.

def naturalsInReals : Set ℝ

Example 0.3.3: Standard sets of numbers: the naturals ℕ, integers ℤ, rationals ℚ, even naturals {2m}, and reals ℝ, with inclusions ℕ ⊆ ℤ ⊆ ℚ ⊆ ℝ.

Equations

• naturalsInReals = Set.range fun (n : ℕ) => ↑n

def integersInReals : Set ℝ

Example 0.3.3 (continued).

Equations

• integersInReals = Set.range fun (z : ℤ) => ↑z

def rationalsInReals : Set ℝ

Example 0.3.3 (continued).

Equations

• rationalsInReals = Set.range fun (q : ℚ) => ↑q

def evenNaturalsInReals : Set ℝ

Example 0.3.3 (continued).

Equations

• evenNaturalsInReals = Set.range fun (m : ℕ) => 2 * ↑m

theorem naturalsInReals_subset_integersInReals : naturalsInReals ⊆ integersInReals

Example 0.3.3: The canonical embeddings realize the chain ℕ ⊆ ℤ ⊆ ℚ ⊆ ℝ.

theorem integersInReals_subset_rationalsInReals : integersInReals ⊆ rationalsInReals

Example 0.3.3 (continued).

theorem rationalsInReals_subset_reals : rationalsInReals ⊆ Set.univ

Example 0.3.3 (continued).

@[reducible, inline]

abbrev unionElementCollection {α : Type u} (A B : ElementCollection α) : ElementCollection α

Definition 0.3.4: (i) union A ∪ B = {x : x ∈ A ∨ x ∈ B}; (ii) intersection A ∩ B = {x : x ∈ A ∧ x ∈ B}; (iii) relative complement (set difference) A \ B = {x : x ∈ A ∧ x ∉ B}; (iv) complement Bᶜ means the difference from the ambient universe or an understood superset; (v) sets are disjoint when their intersection is empty.

Equations

• unionElementCollection A B = A ∪ B

theorem mem_unionElementCollection {α : Type u} {A B : ElementCollection α} {x : α} : x ∈ unionElementCollection A B ↔ x ∈ A ∨ x ∈ B

@[reducible, inline]

abbrev intersectionElementCollection {α : Type u} (A B : ElementCollection α) : ElementCollection α

Equations

• intersectionElementCollection A B = A ∩ B

theorem mem_intersectionElementCollection {α : Type u} {A B : ElementCollection α} {x : α} : x ∈ intersectionElementCollection A B ↔ x ∈ A ∧ x ∈ B

@[reducible, inline]

abbrev relativeComplementElementCollection {α : Type u} (A B : ElementCollection α) : ElementCollection α

Equations

• relativeComplementElementCollection A B = A \ B

theorem mem_relativeComplementElementCollection {α : Type u} {A B : ElementCollection α} {x : α} : x ∈ relativeComplementElementCollection A B ↔ x ∈ A ∧ x ∉ B

@[reducible, inline]

abbrev complementElementCollection {α : Type u} (B : ElementCollection α) : ElementCollection α

Equations

• complementElementCollection B = Set.compl B

theorem mem_complementElementCollection {α : Type u} {B : ElementCollection α} {x : α} : x ∈ complementElementCollection B ↔ x ∉ B

@[reducible, inline]

abbrev disjointElementCollections {α : Type u} (A B : ElementCollection α) : Prop

Equations

• disjointElementCollections A B = Disjoint A B

theorem disjointElementCollections_iff {α : Type u} {A B : ElementCollection α} : disjointElementCollections A B ↔ A ∩ B = ∅

theorem deMorgan_compl_union {α : Type u} {B C : Set α} : (B ∪ C)ᶜ = Bᶜ ∩ Cᶜ

theorem deMorgan_compl_inter {α : Type u} {B C : Set α} : (B ∩ C)ᶜ = Bᶜ ∪ Cᶜ

theorem deMorgan_diff_union {α : Type u} {A B C : Set α} : A \ (B ∪ C) = A \ B ∩ (A \ C)

theorem deMorgan_diff_inter {α : Type u} {A B C : Set α} : A \ (B ∩ C) = A \ B ∪ A \ C

theorem deMorgan_sets {α : Type u} {A B C : Set α} : (B ∪ C)ᶜ = Bᶜ ∩ Cᶜ ∧ (B ∩ C)ᶜ = Bᶜ ∪ Cᶜ ∧ A \ (B ∪ C) = A \ B ∩ (A \ C) ∧ A \ (B ∩ C) = A \ B ∪ A \ C

Theorem 0.3.5 (DeMorgan). For sets A, B, C, (B ∪ C)ᶜ = Bᶜ ∩ Cᶜ and (B ∩ C)ᶜ = Bᶜ ∪ Cᶜ; more generally, A \ (B ∪ C) = (A \ B) ∩ (A \ C) and A \ (B ∩ C) = (A \ B) ∪ (A \ C).