Introduction to Real Analysis, Volume I (Jiri Lebl, 2025) -- Chapter 00 -- Section 03 -- Part 1

open scoped BigOperatorssection Chap00section Section03universe u v wvariable {α : Type u} {β : Type v} {γ : Type w}

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 ∅ : ?m.1∅ (or ∅ : ?m.3{}).

abbrev ElementCollection (α : Type u) := Set α

The empty set from Definition 0.3.1 is mathlib's ∅ : ?m.1∅.

abbrev emptyElementCollection (α : Type u) : ElementCollection α := (∅ : Set α)

The book's notion of set coincides with mathlib's Set.{u} (α : Type u) : Type uSet.

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

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

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

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

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

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

theorem elementCollection_eq_iff_subset_subset {α : Type u} {A B : ElementCollection α} : A = B ↔ subsetElementCollection A B ∧ subsetElementCollection B A := by constructor · intro h subst h constructor · intro x hx exact hx · intro x hx exact hx · intro h apply Set.ext intro x constructor · intro hx exact h.1 hx · intro hx exact h.2 hx

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

abbrev properSubsetElementCollection {α : Type u} (A B : ElementCollection α) : Prop := subsetElementCollection A B ∧ A ≠ B

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

theorem properSubsetElementCollection_iff {α : Type u} {A B : ElementCollection α} : properSubsetElementCollection A B ↔ A ⊂ B := by constructor · intro h exact ssubset_of_subset_of_ne h.1 h.2 · intro h rcases (ssubset_iff_subset_ne).1 h with ⟨hAB, hne⟩ exact ⟨hAB, hne⟩

Example 0.3.3: Standard sets of numbers: the naturals ℕ : Typeℕ, integers ℤ : Typeℤ, rationals ℚ : Typeℚ, even naturals , and reals ℝ : Typeℝ, with inclusions .

def naturalsInReals : Set ℝ := Set.range fun n : ℕ => (n : ℝ)

Example 0.3.3 (continued).

def integersInReals : Set ℝ := Set.range fun z : ℤ => (z : ℝ)

Example 0.3.3 (continued).

def rationalsInReals : Set ℝ := Set.range fun q : ℚ => (q : ℝ)

Example 0.3.3 (continued).

def evenNaturalsInReals : Set ℝ := Set.range fun m : ℕ => (2 * m : ℝ)

Example 0.3.3: The canonical embeddings realize the chain .

theorem naturalsInReals_subset_integersInReals : naturalsInReals ⊆ integersInReals := by intro x hx rcases hx with ⟨n, rfl⟩ refine ⟨(n : ℤ), ?_⟩ norm_cast

Example 0.3.3 (continued).

theorem integersInReals_subset_rationalsInReals : integersInReals ⊆ rationalsInReals := by intro x hx rcases hx with ⟨z, rfl⟩ refine ⟨(z : ℚ), ?_⟩ norm_cast

Example 0.3.3 (continued).

theorem rationalsInReals_subset_reals : rationalsInReals ⊆ (Set.univ : Set ℝ) := by intro x hx exact Set.mem_univ x

Definition 0.3.4: (i) union Unknown identifier `A`A ∪ Unknown identifier `B`B = {x : Unknown identifier `x`x ∈ Unknown identifier `A`A ∨ Unknown identifier `x`x ∈ Unknown identifier `B`B}; (ii) intersection Unknown identifier `A`A ∩ Unknown identifier `B`B = Fields missing: `left`, `right` Hint: Add missing fields: ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲l̲e̲f̲t̲ ̲:̲=̲ ̲_̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲r̲i̲g̲h̲t̲ ̲:̲=̲ ̲_̲{`x` is not a field of structure `And`x : Unknown identifier `x`x ∈ Unknown identifier `A`A ∧ Unknown identifier `x`x ∈ Unknown identifier `B`B}; (iii) relative complement (set difference) A \ B = {x : x ∈ A ∧ x ∉ B}; (iv) complement Unknown identifier `B`sorryᶜ : ?m.1Bᶜ means the difference from the ambient universe or an understood superset; (v) sets are disjoint when their intersection is empty.

abbrev unionElementCollection (A B : ElementCollection α) : ElementCollection α := A ∪ B
theorem mem_unionElementCollection {A B : ElementCollection α} {x : α} : x ∈ unionElementCollection A B ↔ x ∈ A ∨ x ∈ B := by simp [unionElementCollection]abbrev intersectionElementCollection (A B : ElementCollection α) : ElementCollection α := A ∩ Btheorem mem_intersectionElementCollection {A B : ElementCollection α} {x : α} : x ∈ intersectionElementCollection A B ↔ x ∈ A ∧ x ∈ B := by simp [intersectionElementCollection]abbrev relativeComplementElementCollection (A B : ElementCollection α) : ElementCollection α := A \ Btheorem mem_relativeComplementElementCollection {A B : ElementCollection α} {x : α} : x ∈ relativeComplementElementCollection A B ↔ x ∈ A ∧ x ∉ B := by simp [relativeComplementElementCollection]abbrev complementElementCollection (B : ElementCollection α) : ElementCollection α := Set.compl Btheorem mem_complementElementCollection {B : ElementCollection α} {x : α} : x ∈ complementElementCollection B ↔ x ∉ B := by rflabbrev disjointElementCollections (A B : ElementCollection α) : Prop := Disjoint A Btheorem disjointElementCollections_iff {A B : ElementCollection α} : disjointElementCollections A B ↔ A ∩ B = (∅ : Set α) := by simpa [disjointElementCollections] using (Set.disjoint_iff_inter_eq_empty : Disjoint A B ↔ A ∩ B = (∅ : Set α))-- Helper lemmas for De Morgan identities on sets. lemma deMorgan_compl_union {B C : Set α} : (B ∪ C)ᶜ = Bᶜ ∩ Cᶜ := by simplemma deMorgan_compl_inter {B C : Set α} : (B ∩ C)ᶜ = Bᶜ ∪ Cᶜ := by simpa using (Set.compl_inter B C)lemma deMorgan_diff_union {A B C : Set α} : A \ (B ∪ C) = (A \ B) ∩ (A \ C) := by ext x simp [Set.mem_diff, not_or, and_left_comm, and_assoc]lemma deMorgan_diff_inter {A B C : Set α} : A \ (B ∩ C) = (A \ B) ∪ (A \ C) := by classical ext x simp tauto

Theorem 0.3.5 (DeMorgan). For sets Unknown identifier `A`A, Unknown identifier `B`B, Unknown identifier `C`C, (sorry ∪ sorry)ᶜ = sorryᶜ ∩ sorryᶜ : Prop(Unknown identifier `B`B ∪ Unknown identifier `C`C)ᶜ = Unknown identifier `B`Bᶜ ∩ Unknown identifier `C`Cᶜ and (sorry ∩ sorry)ᶜ = sorryᶜ ∪ sorryᶜ : Prop(Unknown identifier `B`B ∩ Unknown identifier `C`C)ᶜ = Unknown identifier `B`Bᶜ ∪ Unknown identifier `C`Cᶜ; more generally, Unknown identifier `A`sorry \ (sorry ∪ sorry) = sorry \ sorry ∩ (sorry \ sorry) : PropA \ (Unknown identifier `B`B ∪ Unknown identifier `C`C) = (Unknown identifier `A`A \ Unknown identifier `B`B) ∩ (Unknown identifier `A`A \ Unknown identifier `C`C) and Unknown identifier `A`sorry \ (sorry ∩ sorry) = sorry \ sorry ∪ sorry \ sorry : PropA \ (Unknown identifier `B`B ∩ Unknown identifier `C`C) = (Unknown identifier `A`A \ Unknown identifier `B`B) ∪ (Unknown identifier `A`A \ Unknown identifier `C`C).

theorem deMorgan_sets {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) := by refine ⟨deMorgan_compl_union, ?_⟩ refine ⟨deMorgan_compl_inter, ?_⟩ exact ⟨deMorgan_diff_union, deMorgan_diff_inter⟩
end Section03end Chap00