Analysis I, Section 9.1: Subsets of the real line

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

• Review of Mathlib intervals.
• Adherent points, limit points, isolated points.
• Closed sets and closure.
• The Heine-Borel theorem for the real line.

@[reducible, inline]

abbrev Real.adherent' (ε x : ℝ) (X : Set ℝ) : Prop

Definition 9.1.5. Note that a slightly different Real.adherent was defined in Chapter 6.4

Equations

• ε.adherent' x X = ∃ y ∈ X, |x - y| ≤ ε

@[reducible, inline]

abbrev Chapter9.AdherentPt (x : ℝ) (X : Set ℝ) : Prop

Definition 9.1.

Equations

• Chapter9.AdherentPt x X = ∀ ε > 0, ε.adherent' x X

theorem Chapter9.closure_def (X : Set ℝ) : closure X = {x : ℝ | AdherentPt x X}

Definition 9.1.10 (Closure). Here we identify this definition with the Mathilb version.

theorem Chapter9.closure_def' (X : Set ℝ) (x : ℝ) : x ∈ closure X ↔ AdherentPt x X

theorem Chapter9.AdherentPt_def (x : ℝ) (X : Set ℝ) : AdherentPt x X = ClusterPt x (Filter.principal X)

identification of AdherentPt with Mathlib's ClusterPt

theorem Chapter9.subset_closure (X : Set ℝ) : X ⊆ closure X

Lemma 9.1.11 / Exercise 9.1.2

theorem Chapter9.closure_union (X Y : Set ℝ) : closure (X ∪ Y) = closure X ∪ closure Y

Lemma 9.1.11 / Exercise 9.1.2

theorem Chapter9.closure_inter (X Y : Set ℝ) : closure (X ∩ Y) ⊆ closure X ∩ closure Y

Lemma 9.1.11 / Exercise 9.1.2

theorem Chapter9.closure_subset {X Y : Set ℝ} (h : X ⊆ Y) : closure X ⊆ closure Y

Lemma 9.1.11 / Exercise 9.1.2

theorem Chapter9.closure_of_subset_closure {X Y : Set ℝ} (h : X ⊆ Y) (h' : Y ⊆ closure X) : closure Y = closure X

Exercise 9.1.1

theorem Chapter9.closure_of_Ioo {a b : ℝ} (h : a < b) : closure (Set.Ioo a b) = Set.Icc a b

Lemma 9.1.12

theorem Chapter9.closure_of_Ioc {a b : ℝ} (h : a < b) : closure (Set.Ioc a b) = Set.Icc a b

theorem Chapter9.closure_of_Ico {a b : ℝ} (h : a < b) : closure (Set.Ico a b) = Set.Icc a b

theorem Chapter9.closure_of_Icc {a b : ℝ} (h : a ≤ b) : closure (Set.Icc a b) = Set.Icc a b

theorem Chapter9.closure_of_Ioi {a : ℝ} : closure (Set.Ioi a) = Set.Ici a

theorem Chapter9.closure_of_Ici {a : ℝ} : closure (Set.Ici a) = Set.Ici a

theorem Chapter9.closure_of_Iio {a : ℝ} : closure (Set.Iio a) = Set.Iic a

theorem Chapter9.closure_of_Iic {a : ℝ} : closure (Set.Iic a) = Set.Iic a

theorem Chapter9.closure_of_R : closure Set.univ = Set.univ

theorem Chapter9.closure_of_N : closure ((fun (n : ℕ) => ↑n) '' Set.univ) = (fun (n : ℕ) => ↑n) '' Set.univ

Lemma 9.1.13 / Exercise 9.1.3

theorem Chapter9.closure_of_Z : closure ((fun (n : ℤ) => ↑n) '' Set.univ) = (fun (n : ℤ) => ↑n) '' Set.univ

Lemma 9.1.13 / Exercise 9.1.3

theorem Chapter9.closure_of_Q : closure ((fun (n : ℚ) => ↑n) '' Set.univ) = Set.univ

Lemma 9.1.13 / Exercise 9.1.3

theorem Chapter9.limit_of_AdherentPt (X : Set ℝ) (x : ℝ) : AdherentPt x X ↔ ∃ (a : ℕ → ℝ), (∀ (n : ℕ), a n ∈ X) ∧ Filter.Tendsto a Filter.atTop (nhds x)

Lemma 9.1.14 / Exercise 9.1.5

theorem Chapter9.AdherentPt.of_mem {X : Set ℝ} {x : ℝ} (h : x ∈ X) : AdherentPt x X

theorem Chapter9.isClosed_def (X : Set ℝ) : IsClosed X ↔ closure X = X

Definition 9.1.15. Here we use the Mathlib definition.

theorem Chapter9.isClosed_def' (X : Set ℝ) : IsClosed X ↔ ∀ (x : ℝ), AdherentPt x X → x ∈ X

theorem Chapter9.Icc_closed {a b : ℝ} : IsClosed (Set.Icc a b)

Examples 9.1.16

theorem Chapter9.Ici_closed (a : ℝ) : IsClosed (Set.Ici a)

Examples 9.1.16

theorem Chapter9.Iic_closed (a : ℝ) : IsClosed (Set.Iic a)

Examples 9.1.16

theorem Chapter9.R_closed : IsClosed Set.univ

Examples 9.1.16

theorem Chapter9.Ico_not_closed {a b : ℝ} (h : a < b) : ¬IsClosed (Set.Ico a b)

Examples 9.1.16

theorem Chapter9.Ioc_not_closed {a b : ℝ} (h : a < b) : ¬IsClosed (Set.Ioc a b)

Examples 9.1.16

theorem Chapter9.Ioo_not_closed {a b : ℝ} (h : a < b) : ¬IsClosed (Set.Ioo a b)

Examples 9.1.16

theorem Chapter9.Ioi_not_closed (a : ℝ) : ¬IsClosed (Set.Ioi a)

Examples 9.1.16

theorem Chapter9.Iio_not_closed (a : ℝ) : ¬IsClosed (Set.Iio a)

Examples 9.1.16

theorem Chapter9.N_closed : IsClosed ((fun (n : ℕ) => ↑n) '' Set.univ)

Examples 9.1.16

theorem Chapter9.Z_closed : IsClosed ((fun (n : ℤ) => ↑n) '' Set.univ)

Examples 9.1.16

theorem Chapter9.Q_not_closed : ¬IsClosed ((fun (n : ℚ) => ↑n) '' Set.univ)

Examples 9.1.16

theorem Chapter9.isClosed_iff_limits_mem (X : Set ℝ) : IsClosed X ↔ ∀ (a : ℕ → ℝ) (L : ℝ), (∀ (n : ℕ), a n ∈ X) → Filter.Tendsto a Filter.atTop (nhds L) → L ∈ X

Corollary 9.1.17

@[reducible, inline]

abbrev Chapter9.LimitPt (x : ℝ) (X : Set ℝ) : Prop

Definition 9.1.18 (Limit points)

Equations

• Chapter9.LimitPt x X = Chapter9.AdherentPt x (X \ {x})

theorem Chapter9.LimitPt.iff_AccPt (x : ℝ) (X : Set ℝ) : LimitPt x X ↔ AccPt x (Filter.principal X)

Identification with Mathlib's AccPt

@[reducible, inline]

abbrev Chapter9.IsolatedPt (x : ℝ) (X : Set ℝ) : Prop

Definition 9.1.18 (Isolated points)

Equations

• Chapter9.IsolatedPt x X = (x ∈ X ∧ ∃ ε > 0, ∀ y ∈ X \ {x}, |x - y| > ε)

theorem Chapter9.LimitPt.iff_limit (x : ℝ) (X : Set ℝ) : LimitPt x X ↔ ∃ (a : ℕ → ℝ), (∀ (n : ℕ), a n ∈ X \ {x}) ∧ Filter.Tendsto a Filter.atTop (nhds x)

Remark 9.1.20

theorem Chapter9.mem_Icc_isLimit {a b x : ℝ} (h : a < b) (hx : x ∈ Set.Icc a b) : LimitPt x (Set.Icc a b)

Lemma 9.1.21

theorem Chapter9.mem_Ico_isLimit {a b x : ℝ} (hx : x ∈ Set.Ico a b) : LimitPt x (Set.Ico a b)

theorem Chapter9.mem_Ioc_isLimit {a b x : ℝ} (hx : x ∈ Set.Ioc a b) : LimitPt x (Set.Ioc a b)

theorem Chapter9.mem_Ioo_isLimit {a b x : ℝ} (hx : x ∈ Set.Ioo a b) : LimitPt x (Set.Ioo a b)

theorem Chapter9.mem_Ici_isLimit {a x : ℝ} (hx : x ∈ Set.Ici a) : LimitPt x (Set.Ici a)

theorem Chapter9.mem_Ioi_isLimit {a x : ℝ} (hx : x ∈ Set.Ioi a) : LimitPt x (Set.Ioi a)

theorem Chapter9.mem_Iic_isLimit {a x : ℝ} (hx : x ∈ Set.Iic a) : LimitPt x (Set.Iic a)

theorem Chapter9.mem_Iio_isLimit {a x : ℝ} (hx : x ∈ Set.Iio a) : LimitPt x (Set.Iio a)

theorem Chapter9.mem_R_isLimit {x : ℝ} : LimitPt x Set.univ

theorem Chapter9.isBounded_def (X : Set ℝ) : Bornology.IsBounded X ↔ ∃ M > 0, X ⊆ Set.Icc (-M) M

Definition 9.1.22. We use here Mathlib's Bornology.IsBounded

theorem Chapter9.Icc_bounded (a b : ℝ) : Bornology.IsBounded (Set.Icc a b)

Example 9.1.23

theorem Chapter9.Ici_unbounded (a : ℝ) : ¬Bornology.IsBounded (Set.Ici a)

Example 9.1.23

theorem Chapter9.N_unbounded (a : ℝ) : ¬Bornology.IsBounded ((fun (n : ℕ) => ↑n) '' Set.univ)

Example 9.1.23

theorem Chapter9.Z_unbounded (a : ℝ) : ¬Bornology.IsBounded ((fun (n : ℤ) => ↑n) '' Set.univ)

Example 9.1.23

theorem Chapter9.Q_unbounded (a : ℝ) : ¬Bornology.IsBounded ((fun (n : ℚ) => ↑n) '' Set.univ)

Example 9.1.23

theorem Chapter9.R_unbounded (a : ℝ) : ¬Bornology.IsBounded Set.univ

Example 9.1.23

theorem Chapter9.Heine_Borel (X : Set ℝ) : IsClosed X ∧ Bornology.IsBounded X ↔ ∀ (a : ℕ → ℝ), (∀ (n : ℕ), a n ∈ X) → ∃ (n : ℕ → ℕ), StrictMono n ∧ ∃ L ∈ X, Filter.Tendsto (fun (j : ℕ) => a (n j)) Filter.atTop (nhds L)

Theorem 9.1.24 / Exercise 9.1.13 (Heine-Borel theorem for the line)