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.

variable (I : Type*)

Set.Icc_def.{u_1} {α : Type u_1} [Preorder α] (a b : α) : {x | a ≤ x ∧ x ≤ b} = Set.Icc a b

Set.Ico_def.{u_1} {α : Type u_1} [Preorder α] (a b : α) : {x | a ≤ x ∧ x < b} = Set.Ico a b

Set.Ioc_def.{u_1} {α : Type u_1} [Preorder α] (a b : α) : {x | a < x ∧ x ≤ b} = Set.Ioc a b

Set.Ioo_def.{u_1} {α : Type u_1} [Preorder α] (a b : α) : {x | a < x ∧ x < b} = Set.Ioo a b

Set.Ici_def.{u_1} {α : Type u_1} [Preorder α] (a : α) : {x | a ≤ x} = Set.Ici a

Set.Ioi_def.{u_1} {α : Type u_1} [Preorder α] (a : α) : {x | a < x} = Set.Ioi a

Set.Iic_def.{u_1} {α : Type u_1} [Preorder α] (b : α) : {x | x ≤ b} = Set.Iic b

Set.Iio_def.{u_1} {α : Type u_1} [Preorder α] (a : α) : {x | x < a} = Set.Iio a

EReal.image_coe_Icc (x y : ℝ) : Real.toEReal '' Set.Icc x y = Set.Icc ↑x ↑y

EReal.image_coe_Ico (x y : ℝ) : Real.toEReal '' Set.Ico x y = Set.Ico ↑x ↑y

EReal.image_coe_Ioc (x y : ℝ) : Real.toEReal '' Set.Ioc x y = Set.Ioc ↑x ↑y

EReal.image_coe_Ioo (x y : ℝ) : Real.toEReal '' Set.Ioo x y = Set.Ioo ↑x ↑y

EReal.image_coe_Ici (x : ℝ) : Real.toEReal '' Set.Ici x = Set.Ico ↑x ⊤

EReal.image_coe_Ioi (x : ℝ) : Real.toEReal '' Set.Ioi x = Set.Ioo ↑x ⊤

EReal.image_coe_Iic (x : ℝ) : Real.toEReal '' Set.Iic x = Set.Ioc ⊥ ↑x

EReal.image_coe_Iio (x : ℝ) : Real.toEReal '' Set.Iio x = Set.Ioo ⊥ ↑x

Example 9.1.4

declaration uses 'sorry'example {a b: EReal} (h: a > b) : Set.Icc a b = ∅ := byI:Type u_1a:ERealb:ERealh:a > b⊢ Set.Icc a b = ∅
  sorryAll goals completed! 🐙

declaration uses 'sorry'example {a b: EReal} (h: a ≥ b) : Set.Ico a b = ∅ := byI:Type u_1a:ERealb:ERealh:a ≥ b⊢ Set.Ico a b = ∅
  sorryAll goals completed! 🐙

declaration uses 'sorry'example {a b: EReal} (h: a ≥ b) : Set.Ioc a b = ∅ := byI:Type u_1a:ERealb:ERealh:a ≥ b⊢ Set.Ioc a b = ∅
  sorryAll goals completed! 🐙

declaration uses 'sorry'example {a b: EReal} (h: a ≥ b) : Set.Ioo a b = ∅ := byI:Type u_1a:ERealb:ERealh:a ≥ b⊢ Set.Ioo a b = ∅
  sorryAll goals completed! 🐙

declaration uses 'sorry'example {a b: EReal} (h: a = b) : Set.Icc a a = {a} := byI:Type u_1a:ERealb:ERealh:a = b⊢ Set.Icc a a = {a}
  sorryAll goals completed! 🐙

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

abbrev Real.adherent' (ε:ℝ) (x:ℝ) (X: Set ℝ) := ∃ y ∈ X, |x - y| ≤ ε

Example 9.1.7

declaration uses 'sorry'example : (0.5:ℝ).adherent' 1.1 (.Ioo 0 1) := byI:Type u_1⊢ Real.adherent' 0.5 1.1 (Set.Ioo 0 1) sorryAll goals completed! 🐙

declaration uses 'sorry'example : ¬ (0.1:ℝ).adherent' 1.1 (.Ioo 0 1) := byI:Type u_1⊢ ¬Real.adherent' 0.1 1.1 (Set.Ioo 0 1) sorryAll goals completed! 🐙

declaration uses 'sorry'example : (0.5:ℝ).adherent' 1.1 {1,2,3} := byI:Type u_1⊢ Real.adherent' 0.5 1.1 {1, 2, 3} sorryAll goals completed! 🐙

namespace Chapter9

Definition 9.1.

abbrev AdherentPt (x:ℝ) (X:Set ℝ) := ∀ ε > (0:ℝ), ε.adherent' x X

declaration uses 'sorry'example : AdherentPt 1 (.Ioo 0 1) := byI:Type u_1⊢ AdherentPt 1 (Set.Ioo 0 1) sorryAll goals completed! 🐙

declaration uses 'sorry'example : ¬ AdherentPt 2 (.Ioo 0 1) := byI:Type u_1⊢ ¬AdherentPt 2 (Set.Ioo 0 1) sorryAll goals completed! 🐙

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

theorem closure_def (X:Set ℝ) : closure X = { x | AdherentPt x X } := byX:Set ℝ⊢ closure X = {x | AdherentPt x X}
  exthX:Set ℝx✝:ℝ⊢ x✝ ∈ closure X ↔ x✝ ∈ {x | AdherentPt x X}; simp [Real.mem_closure_iff, AdherentPt, Real.adherent']hX:Set ℝx✝:ℝ⊢ (∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |y - x✝| < ε) ↔ ∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |x✝ - y| ≤ ε
  constructorh.mpX:Set ℝx✝:ℝ⊢ (∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |y - x✝| < ε) → ∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |x✝ - y| ≤ εh.mprX:Set ℝx✝:ℝ⊢ (∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |x✝ - y| ≤ ε) → ∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |y - x✝| < ε <;>h.mpX:Set ℝx✝:ℝ⊢ (∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |y - x✝| < ε) → ∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |x✝ - y| ≤ εh.mprX:Set ℝx✝:ℝ⊢ (∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |x✝ - y| ≤ ε) → ∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |y - x✝| < ε intro h ε hεh.mprX:Set ℝx✝:ℝh:∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |x✝ - y| ≤ εε:ℝhε:0 < ε⊢ ∃ y ∈ X, |y - x✝| < ε
  all_goals choose y hy hxy using h _ (half_pos hε)h.mprX:Set ℝx✝:ℝh:∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |x✝ - y| ≤ εε:ℝhε:0 < εy:ℝhy:y ∈ Xhxy:|x✝ - y| ≤ ε / 2⊢ ∃ y ∈ X, |y - x✝| < ε; exact ⟨ _, hy, byX:Set ℝx✝:ℝh:∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |x✝ - y| ≤ εε:ℝhε:0 < εy:ℝhy:y ∈ Xhxy:|x✝ - y| ≤ ε / 2⊢ |y - x✝| < ε rw [abs_sub_comm]X:Set ℝx✝:ℝh:∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |x✝ - y| ≤ εε:ℝhε:0 < εy:ℝhy:y ∈ Xhxy:|x✝ - y| ≤ ε / 2⊢ |x✝ - y| < ε; linarithAll goals completed! 🐙 ⟩

theorem closure_def' (X:Set ℝ) (x :ℝ) : x ∈ closure X ↔ AdherentPt x X := byX:Set ℝx:ℝ⊢ x ∈ closure X ↔ AdherentPt x X
  simp [closure_def]All goals completed! 🐙

identification of Chapter9.AdherentPt (x : ℝ) (X : Set ℝ) : PropAdherentPt with Mathlib's ClusterPt.{u_1} {X : Type u_1} [TopologicalSpace X] (x : X) (F : Filter X) : PropClusterPt

theorem AdherentPt_def (x:ℝ) (X:Set ℝ) : AdherentPt x X = ClusterPt x (.principal X) := byx:ℝX:Set ℝ⊢ AdherentPt x X = ClusterPt x (Filter.principal X)
  rw [←closure_def', mem_closure_iff_clusterPt]All goals completed! 🐙

Lemma 9.1.11 / Exercise 9.1.2

theorem declaration uses 'sorry'subset_closure (X:Set ℝ): X ⊆ closure X := byX:Set ℝ⊢ X ⊆ closure X sorryAll goals completed! 🐙

Lemma 9.1.11 / Exercise 9.1.2

theorem declaration uses 'sorry'closure_union (X Y:Set ℝ): closure (X ∪ Y) = closure X ∪ closure Y := byX:Set ℝY:Set ℝ⊢ closure (X ∪ Y) = closure X ∪ closure Y sorryAll goals completed! 🐙

Lemma 9.1.11 / Exercise 9.1.2

theorem declaration uses 'sorry'closure_inter (X Y:Set ℝ): closure (X ∩ Y) ⊆ closure X ∩ closure Y := byX:Set ℝY:Set ℝ⊢ closure (X ∩ Y) ⊆ closure X ∩ closure Y sorryAll goals completed! 🐙

Lemma 9.1.11 / Exercise 9.1.2

theorem declaration uses 'sorry'closure_subset {X Y:Set ℝ} (h: X ⊆ Y): closure X ⊆ closure Y := byX:Set ℝY:Set ℝh:X ⊆ Y⊢ closure X ⊆ closure Y sorryAll goals completed! 🐙

Exercise 9.1.1

theorem declaration uses 'sorry'closure_of_subset_closure {X Y:Set ℝ} (h: X ⊆ Y) (h' : Y ⊆ closure X): closure Y = closure X := byX:Set ℝY:Set ℝh:X ⊆ Yh':Y ⊆ closure X⊢ closure Y = closure X sorryAll goals completed! 🐙

Lemma 9.1.12

theorem declaration uses 'sorry'closure_of_Ioo {a b:ℝ} (h:a < b) : closure (.Ioo a b) = .Icc a b := bya:ℝb:ℝh:a < b⊢ closure (Set.Ioo a b) = Set.Icc a b
  -- This proof is written to follow the structure of the original text.
  ext xha:ℝb:ℝh:a < bx:ℝ⊢ x ∈ closure (Set.Ioo a b) ↔ x ∈ Set.Icc a b; simp [closure_def, AdherentPt, Real.adherent']ha:ℝb:ℝh:a < bx:ℝ⊢ (∀ (ε : ℝ), 0 < ε → ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ ε) ↔ a ≤ x ∧ x ≤ b
  constructorh.mpa:ℝb:ℝh:a < bx:ℝ⊢ (∀ (ε : ℝ), 0 < ε → ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ ε) → a ≤ x ∧ x ≤ bh.mpra:ℝb:ℝh:a < bx:ℝ⊢ a ≤ x ∧ x ≤ b → ∀ (ε : ℝ), 0 < ε → ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ ε
  .h.mpa:ℝb:ℝh:a < bx:ℝ⊢ (∀ (ε : ℝ), 0 < ε → ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ ε) → a ≤ x ∧ x ≤ b intro hh.mpa:ℝb:ℝh✝:a < bx:ℝh:∀ (ε : ℝ), 0 < ε → ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ ε⊢ a ≤ x ∧ x ≤ b; contrapose! hh.mpa:ℝb:ℝh✝:a < bx:ℝh:a ≤ x → b < x⊢ ∃ ε, 0 < ε ∧ ∀ (y : ℝ), a < y ∧ y < b → ε < |x - y|
    obtain h' | h' := le_or_gt a xh.mp.inla:ℝb:ℝh✝:a < bx:ℝh:a ≤ x → b < xh':a ≤ x⊢ ∃ ε, 0 < ε ∧ ∀ (y : ℝ), a < y ∧ y < b → ε < |x - y|h.mp.inra:ℝb:ℝh✝:a < bx:ℝh:a ≤ x → b < xh':x < a⊢ ∃ ε, 0 < ε ∧ ∀ (y : ℝ), a < y ∧ y < b → ε < |x - y|
    .h.mp.inla:ℝb:ℝh✝:a < bx:ℝh:a ≤ x → b < xh':a ≤ x⊢ ∃ ε, 0 < ε ∧ ∀ (y : ℝ), a < y ∧ y < b → ε < |x - y| specialize h h'h.mp.inla:ℝb:ℝh✝:a < bx:ℝh':a ≤ xh:b < x⊢ ∃ ε, 0 < ε ∧ ∀ (y : ℝ), a < y ∧ y < b → ε < |x - y|
      use x-b, bya:ℝb:ℝh✝:a < bx:ℝh':a ≤ xh:b < x⊢ 0 < x - b linarithAll goals completed! 🐙
      intro y ⟨ _, _ ⟩righta:ℝb:ℝh✝:a < bx:ℝh':a ≤ xh:b < xy:ℝleft✝:a < yright✝:y < b⊢ x - b < |x - y|; observe : x-y ≤ |x-y|righta:ℝb:ℝh✝:a < bx:ℝh':a ≤ xh:b < xy:ℝleft✝:a < yright✝:y < bthis:x - y ≤ |x - y|⊢ x - b < |x - y|; linarithAll goals completed! 🐙
    use a-x, bya:ℝb:ℝh✝:a < bx:ℝh:a ≤ x → b < xh':x < a⊢ 0 < a - x linarithAll goals completed! 🐙
    intro y ⟨ _, _ ⟩righta:ℝb:ℝh✝:a < bx:ℝh:a ≤ x → b < xh':x < ay:ℝleft✝:a < yright✝:y < b⊢ a - x < |x - y|; observe : -(x-y) ≤ |x-y|righta:ℝb:ℝh✝:a < bx:ℝh:a ≤ x → b < xh':x < ay:ℝleft✝:a < yright✝:y < bthis:-(x - y) ≤ |x - y|⊢ a - x < |x - y|; linarithAll goals completed! 🐙
  intro ⟨ h1, h2 ⟩h.mpra:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ b⊢ ∀ (ε : ℝ), 0 < ε → ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ ε
  by_cases ha : x = apos._@._hyg.1459a:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bha:x = a⊢ ∀ (ε : ℝ), 0 < ε → ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ εneg._@._hyg.1459a:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bha:¬x = a⊢ ∀ (ε : ℝ), 0 < ε → ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ ε
  .pos._@._hyg.1459a:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bha:x = a⊢ ∀ (ε : ℝ), 0 < ε → ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ ε sorryAll goals completed! 🐙
  by_cases hb : x = bpos._@._hyg.1494a:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bha:¬x = ahb:x = b⊢ ∀ (ε : ℝ), 0 < ε → ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ εneg._@._hyg.1494a:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bha:¬x = ahb:¬x = b⊢ ∀ (ε : ℝ), 0 < ε → ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ ε
  .pos._@._hyg.1494a:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bha:¬x = ahb:x = b⊢ ∀ (ε : ℝ), 0 < ε → ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ ε sorryAll goals completed! 🐙
  intro ε _neg._@._hyg.1494a:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bha:¬x = ahb:¬x = bε:ℝa✝:0 < ε⊢ ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ ε; use x, (bya:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bha:¬x = ahb:¬x = bε:ℝa✝:0 < ε⊢ a < x ∧ x < b grindAll goals completed! 🐙); simprighta:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bha:¬x = ahb:¬x = bε:ℝa✝:0 < ε⊢ 0 ≤ ε; orderAll goals completed! 🐙

theorem declaration uses 'sorry'closure_of_Ioc {a b:ℝ} (h:a < b) : closure (.Ioc a b) = .Icc a b := bya:ℝb:ℝh:a < b⊢ closure (Set.Ioc a b) = Set.Icc a b
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'closure_of_Ico {a b:ℝ} (h:a < b) : closure (.Ico a b) = .Icc a b := bya:ℝb:ℝh:a < b⊢ closure (Set.Ico a b) = Set.Icc a b
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'closure_of_Icc {a b:ℝ} (h:a ≤ b) : closure (.Icc a b) = .Icc a b := bya:ℝb:ℝh:a ≤ b⊢ closure (Set.Icc a b) = Set.Icc a b
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'closure_of_Ioi {a:ℝ} : closure (.Ioi a) = .Ici a := bya:ℝ⊢ closure (Set.Ioi a) = Set.Ici a
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'closure_of_Ici {a:ℝ} : closure (.Ici a) = .Ici a := bya:ℝ⊢ closure (Set.Ici a) = Set.Ici a
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'closure_of_Iio {a:ℝ} : closure (.Iio a) = .Iic a := bya:ℝ⊢ closure (Set.Iio a) = Set.Iic a
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'closure_of_Iic {a:ℝ} : closure (.Iic a) = .Iic a := bya:ℝ⊢ closure (Set.Iic a) = Set.Iic a
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'closure_of_R : closure (.univ: Set ℝ) = .univ := by⊢ closure Set.univ = Set.univ sorryAll goals completed! 🐙

Lemma 9.1.13 / Exercise 9.1.3

theorem declaration uses 'sorry'closure_of_N :
  closure ((fun n:ℕ ↦ (n:ℝ)) '' .univ) = ((fun n:ℕ ↦ (n:ℝ)) '' .univ) := by⊢ closure ((fun n => ↑n) '' Set.univ) = (fun n => ↑n) '' Set.univ
    sorryAll goals completed! 🐙

Lemma 9.1.13 / Exercise 9.1.3

theorem declaration uses 'sorry'closure_of_Z :
  closure ((fun n:ℤ ↦ (n:ℝ)) '' .univ) = ((fun n:ℤ ↦ (n:ℝ)) '' .univ) := by⊢ closure ((fun n => ↑n) '' Set.univ) = (fun n => ↑n) '' Set.univ
    sorryAll goals completed! 🐙

Lemma 9.1.13 / Exercise 9.1.3

theorem declaration uses 'sorry'closure_of_Q :
  closure ((fun n:ℚ ↦ (n:ℝ)) '' .univ) = .univ := by⊢ closure ((fun n => ↑n) '' Set.univ) = Set.univ
    sorryAll goals completed! 🐙

Lemma 9.1.14 / Exercise 9.1.5

theorem declaration uses 'sorry'limit_of_AdherentPt (X: Set ℝ) (x:ℝ) :
  AdherentPt x X ↔ ∃ a : ℕ → ℝ, (∀ n, a n ∈ X) ∧ Filter.atTop.Tendsto a (nhds x) := byX:Set ℝx:ℝ⊢ AdherentPt x X ↔ ∃ a, (∀ (n : ℕ), a n ∈ X) ∧ Filter.Tendsto a Filter.atTop (nhds x)
    sorryAll goals completed! 🐙

theorem AdherentPt.of_mem {X: Set ℝ} {x: ℝ} (h: x ∈ X) : AdherentPt x X := byX:Set ℝx:ℝh:x ∈ X⊢ AdherentPt x X
  rw [limit_of_AdherentPt]X:Set ℝx:ℝh:x ∈ X⊢ ∃ a, (∀ (n : ℕ), a n ∈ X) ∧ Filter.Tendsto a Filter.atTop (nhds x); use fun _ ↦ xhX:Set ℝx:ℝh:x ∈ X⊢ (∀ (n : ℕ), (fun x_1 => x) n ∈ X) ∧ Filter.Tendsto (fun x_1 => x) Filter.atTop (nhds x); simp [h]All goals completed! 🐙

Definition 9.1.15. Here we use the Mathlib definition.

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

theorem isClosed_def' (X:Set ℝ): IsClosed X ↔ ∀ x, AdherentPt x X → x ∈ X := byX:Set ℝ⊢ IsClosed X ↔ ∀ (x : ℝ), AdherentPt x X → x ∈ X
  simp [isClosed_def, subset_antisymm_iff, subset_closure]X:Set ℝ⊢ closure X ⊆ X ↔ ∀ (x : ℝ), AdherentPt x X → x ∈ X; simp [closure_def]X:Set ℝ⊢ {x | AdherentPt x X} ⊆ X ↔ ∀ (x : ℝ), AdherentPt x X → x ∈ X; rflAll goals completed! 🐙

Examples 9.1.16

theorem declaration uses 'sorry'Icc_closed {a b:ℝ} : IsClosed (.Icc a b) := bya:ℝb:ℝ⊢ IsClosed (Set.Icc a b) sorryAll goals completed! 🐙

Examples 9.1.16

theorem declaration uses 'sorry'Ici_closed (a:ℝ) : IsClosed (.Ici a) := bya:ℝ⊢ IsClosed (Set.Ici a) sorryAll goals completed! 🐙

Examples 9.1.16

theorem declaration uses 'sorry'Iic_closed (a:ℝ) : IsClosed (.Iic a) := bya:ℝ⊢ IsClosed (Set.Iic a) sorryAll goals completed! 🐙

Examples 9.1.16

theorem declaration uses 'sorry'R_closed : IsClosed (.univ : Set ℝ) := by⊢ IsClosed Set.univ sorryAll goals completed! 🐙

Examples 9.1.16

theorem declaration uses 'sorry'Ico_not_closed {a b:ℝ} (h: a < b) : ¬ IsClosed (.Ico a b) := bya:ℝb:ℝh:a < b⊢ ¬IsClosed (Set.Ico a b) sorryAll goals completed! 🐙

Examples 9.1.16

theorem declaration uses 'sorry'Ioc_not_closed {a b:ℝ} (h: a < b) : ¬ IsClosed (.Ioc a b) := bya:ℝb:ℝh:a < b⊢ ¬IsClosed (Set.Ioc a b) sorryAll goals completed! 🐙

Examples 9.1.16

theorem declaration uses 'sorry'Ioo_not_closed {a b:ℝ} (h: a < b) : ¬ IsClosed (.Ioo a b) := bya:ℝb:ℝh:a < b⊢ ¬IsClosed (Set.Ioo a b) sorryAll goals completed! 🐙

Examples 9.1.16

theorem declaration uses 'sorry'Ioi_not_closed (a:ℝ) : ¬ IsClosed (.Ioi a) := bya:ℝ⊢ ¬IsClosed (Set.Ioi a) sorryAll goals completed! 🐙

Examples 9.1.16

theorem declaration uses 'sorry'Iio_not_closed (a:ℝ) : ¬ IsClosed (.Iio a) := bya:ℝ⊢ ¬IsClosed (Set.Iio a) sorryAll goals completed! 🐙

Examples 9.1.16

theorem declaration uses 'sorry'N_closed : IsClosed ((fun n:ℕ ↦ (n:ℝ)) '' .univ) := by⊢ IsClosed ((fun n => ↑n) '' Set.univ) sorryAll goals completed! 🐙

Examples 9.1.16

theorem declaration uses 'sorry'Z_closed : IsClosed ((fun n:ℤ ↦ (n:ℝ)) '' .univ) := by⊢ IsClosed ((fun n => ↑n) '' Set.univ) sorryAll goals completed! 🐙

Examples 9.1.16

theorem declaration uses 'sorry'Q_not_closed : ¬ IsClosed ((fun n:ℚ ↦ (n:ℝ)) '' .univ) := by⊢ ¬IsClosed ((fun n => ↑n) '' Set.univ) sorryAll goals completed! 🐙

Corollary 9.1.17

theorem isClosed_iff_limits_mem (X: Set ℝ) :
  IsClosed X ↔ ∀ (a:ℕ → ℝ) (L:ℝ), (∀ n, a n ∈ X) → Filter.atTop.Tendsto a (nhds L) → L ∈ X := byX:Set ℝ⊢ IsClosed X ↔ ∀ (a : ℕ → ℝ) (L : ℝ), (∀ (n : ℕ), a n ∈ X) → Filter.Tendsto a Filter.atTop (nhds L) → L ∈ X
  rw [isClosed_def']X:Set ℝ⊢ (∀ (x : ℝ), AdherentPt x X → x ∈ X) ↔
  ∀ (a : ℕ → ℝ) (L : ℝ), (∀ (n : ℕ), a n ∈ X) → Filter.Tendsto a Filter.atTop (nhds L) → L ∈ X
  constructormpX:Set ℝ⊢ (∀ (x : ℝ), AdherentPt x X → x ∈ X) →
  ∀ (a : ℕ → ℝ) (L : ℝ), (∀ (n : ℕ), a n ∈ X) → Filter.Tendsto a Filter.atTop (nhds L) → L ∈ XmprX:Set ℝ⊢ (∀ (a : ℕ → ℝ) (L : ℝ), (∀ (n : ℕ), a n ∈ X) → Filter.Tendsto a Filter.atTop (nhds L) → L ∈ X) →
  ∀ (x : ℝ), AdherentPt x X → x ∈ X
  .mpX:Set ℝ⊢ (∀ (x : ℝ), AdherentPt x X → x ∈ X) →
  ∀ (a : ℕ → ℝ) (L : ℝ), (∀ (n : ℕ), a n ∈ X) → Filter.Tendsto a Filter.atTop (nhds L) → L ∈ X intro h _ L _ _mpX:Set ℝh:∀ (x : ℝ), AdherentPt x X → x ∈ Xa✝²:ℕ → ℝL:ℝa✝¹:∀ (n : ℕ), a✝² n ∈ Xa✝:Filter.Tendsto a✝² Filter.atTop (nhds L)⊢ L ∈ X; apply h LmpX:Set ℝh:∀ (x : ℝ), AdherentPt x X → x ∈ Xa✝²:ℕ → ℝL:ℝa✝¹:∀ (n : ℕ), a✝² n ∈ Xa✝:Filter.Tendsto a✝² Filter.atTop (nhds L)⊢ AdherentPt L X; rw [limit_of_AdherentPt]mpX:Set ℝh:∀ (x : ℝ), AdherentPt x X → x ∈ Xa✝²:ℕ → ℝL:ℝa✝¹:∀ (n : ℕ), a✝² n ∈ Xa✝:Filter.Tendsto a✝² Filter.atTop (nhds L)⊢ ∃ a, (∀ (n : ℕ), a n ∈ X) ∧ Filter.Tendsto a Filter.atTop (nhds L); solve_by_elimAll goals completed! 🐙
  intro _ _ hxmprX:Set ℝa✝:∀ (a : ℕ → ℝ) (L : ℝ), (∀ (n : ℕ), a n ∈ X) → Filter.Tendsto a Filter.atTop (nhds L) → L ∈ Xx✝:ℝhx:AdherentPt x✝ X⊢ x✝ ∈ X; rw [limit_of_AdherentPt] at hxmprX:Set ℝa✝:∀ (a : ℕ → ℝ) (L : ℝ), (∀ (n : ℕ), a n ∈ X) → Filter.Tendsto a Filter.atTop (nhds L) → L ∈ Xx✝:ℝhx:∃ a, (∀ (n : ℕ), a n ∈ X) ∧ Filter.Tendsto a Filter.atTop (nhds x✝)⊢ x✝ ∈ X; grindAll goals completed! 🐙

Definition 9.1.18 (Limit points)

abbrev LimitPt (x:ℝ) (X: Set ℝ) := AdherentPt x (X \ {x})

Identification with Mathlib's AccPt.{u_1} {X : Type u_1} [TopologicalSpace X] (x : X) (F : Filter X) : PropAccPt

theorem LimitPt.iff_AccPt (x:ℝ) (X: Set ℝ) : LimitPt x X ↔ AccPt x (.principal X) := byx:ℝX:Set ℝ⊢ LimitPt x X ↔ AccPt x (Filter.principal X)
  rw [accPt_principal_iff_clusterPt,←AdherentPt_def]All goals completed! 🐙

Definition 9.1.18 (Isolated points)

abbrev IsolatedPt (x:ℝ) (X: Set ℝ) := x ∈ X ∧ ∃ ε>0, ∀ y ∈ X \ {x}, |x-y| > ε

Example 9.1.19

declaration uses 'sorry'example : AdherentPt 3 ((.Ioo 1 2) ∪ {3}) := byI:Type u_1⊢ AdherentPt 3 (Set.Ioo 1 2 ∪ {3}) sorryAll goals completed! 🐙

declaration uses 'sorry'example : ¬ LimitPt 3 ((.Ioo 1 2) ∪ {3}) := byI:Type u_1⊢ ¬LimitPt 3 (Set.Ioo 1 2 ∪ {3}) sorryAll goals completed! 🐙

declaration uses 'sorry'example : IsolatedPt 3 ((.Ioo 1 2) ∪ {3}) := byI:Type u_1⊢ IsolatedPt 3 (Set.Ioo 1 2 ∪ {3}) sorryAll goals completed! 🐙

Remark 9.1.20

theorem LimitPt.iff_limit (x:ℝ) (X: Set ℝ) :
  LimitPt x X ↔ ∃ a : ℕ → ℝ, (∀ n, a n ∈ X \ {x}) ∧ Filter.atTop.Tendsto a (nhds x) := byx:ℝX:Set ℝ⊢ LimitPt x X ↔ ∃ a, (∀ (n : ℕ), a n ∈ X \ {x}) ∧ Filter.Tendsto a Filter.atTop (nhds x)
  simp [limit_of_AdherentPt]All goals completed! 🐙

Lemma 9.1.21

theorem declaration uses 'sorry'mem_Icc_isLimit {a b x:ℝ} (h: a < b) (hx: x ∈ Set.Icc a b) : LimitPt x (.Icc a b) := bya:ℝb:ℝx:ℝh:a < bhx:x ∈ Set.Icc a b⊢ LimitPt x (Set.Icc a b)
  -- This proof is written to follow the structure of the original text, with some slight simplifications.
  simp at hxa:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ b⊢ LimitPt x (Set.Icc a b)
  rw [LimitPt.iff_limit]a:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ b⊢ ∃ a_1, (∀ (n : ℕ), a_1 n ∈ Set.Icc a b \ {x}) ∧ Filter.Tendsto a_1 Filter.atTop (nhds x)
  obtain hxb | hxb := le_iff_lt_or_eq.1 hx.2inla:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < b⊢ ∃ a_1, (∀ (n : ℕ), a_1 n ∈ Set.Icc a b \ {x}) ∧ Filter.Tendsto a_1 Filter.atTop (nhds x)inra:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x = b⊢ ∃ a_1, (∀ (n : ℕ), a_1 n ∈ Set.Icc a b \ {x}) ∧ Filter.Tendsto a_1 Filter.atTop (nhds x)
  .inla:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < b⊢ ∃ a_1, (∀ (n : ℕ), a_1 n ∈ Set.Icc a b \ {x}) ∧ Filter.Tendsto a_1 Filter.atTop (nhds x) use (fun n:ℕ ↦ (x + 1/(n+(b-x)⁻¹)))ha:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < b⊢ (∀ (n : ℕ), (fun n => x + 1 / (↑n + (b - x)⁻¹)) n ∈ Set.Icc a b \ {x}) ∧
  Filter.Tendsto (fun n => x + 1 / (↑n + (b - x)⁻¹)) Filter.atTop (nhds x)
    constructorh.lefta:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < b⊢ ∀ (n : ℕ), x + 1 / (↑n + (b - x)⁻¹) ∈ Set.Icc a b \ {x}h.righta:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < b⊢ Filter.Tendsto (fun n => x + 1 / (↑n + (b - x)⁻¹)) Filter.atTop (nhds x)
    .h.lefta:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < b⊢ ∀ (n : ℕ), x + 1 / (↑n + (b - x)⁻¹) ∈ Set.Icc a b \ {x} intro nh.lefta:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < bn:ℕ⊢ x + 1 / (↑n + (b - x)⁻¹) ∈ Set.Icc a b \ {x}; simph.lefta:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < bn:ℕ⊢ (a ≤ x + (↑n + (b - x)⁻¹)⁻¹ ∧ x + (↑n + (b - x)⁻¹)⁻¹ ≤ b) ∧ ¬↑n + (b - x)⁻¹ = 0
      have : b - x > 0 := bya:ℝb:ℝx:ℝh:a < bhx:x ∈ Set.Icc a b⊢ LimitPt x (Set.Icc a b) linarithAll goals completed! 🐙
      have : (b - x)⁻¹ > 0 := bya:ℝb:ℝx:ℝh:a < bhx:x ∈ Set.Icc a b⊢ LimitPt x (Set.Icc a b) positivityAll goals completed! 🐙
      have : n + (b - x)⁻¹ > 0 := bya:ℝb:ℝx:ℝh:a < bhx:x ∈ Set.Icc a b⊢ LimitPt x (Set.Icc a b) linarithAll goals completed! 🐙
      have : (n+(b - x)⁻¹)⁻¹ > 0 := bya:ℝb:ℝx:ℝh:a < bhx:x ∈ Set.Icc a b⊢ LimitPt x (Set.Icc a b) positivityAll goals completed! 🐙
      have : (b-x)⁻¹ ≤ n + (b - x)⁻¹ := bya:ℝb:ℝx:ℝh:a < bhx:x ∈ Set.Icc a b⊢ LimitPt x (Set.Icc a b) linarithAll goals completed! 🐙
      have : (n + (b - x)⁻¹)⁻¹ ≤ b-x := bya:ℝb:ℝx:ℝh:a < bhx:x ∈ Set.Icc a b⊢ LimitPt x (Set.Icc a b) rwa [inv_le_comm₀ ?_ ?_]a:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < bn:ℕthis✝³:_fvar.134614 - _fvar.134615 > 0 := ?_mvar.143048this✝²:(_fvar.134614 - _fvar.134615)⁻¹ > 0 := ?_mvar.143475this✝¹:↑_fvar.137254 + (_fvar.134614 - _fvar.134615)⁻¹ > 0 := ?_mvar.145783this✝:(↑_fvar.137254 + (_fvar.134614 - _fvar.134615)⁻¹)⁻¹ > 0 := ?_mvar.148122this:(_fvar.134614 - _fvar.134615)⁻¹ ≤ ↑_fvar.137254 + (_fvar.134614 - _fvar.134615)⁻¹ := ?_mvar.152351⊢ (b - x)⁻¹ ≤ ↑n + (b - x)⁻¹a:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < bn:ℕthis✝³:_fvar.134614 - _fvar.134615 > 0 := ?_mvar.143048this✝²:(_fvar.134614 - _fvar.134615)⁻¹ > 0 := ?_mvar.143475this✝¹:↑_fvar.137254 + (_fvar.134614 - _fvar.134615)⁻¹ > 0 := ?_mvar.145783this✝:(↑_fvar.137254 + (_fvar.134614 - _fvar.134615)⁻¹)⁻¹ > 0 := ?_mvar.148122this:(_fvar.134614 - _fvar.134615)⁻¹ ≤ ↑_fvar.137254 + (_fvar.134614 - _fvar.134615)⁻¹ := ?_mvar.152351⊢ 0 < ↑n + (b - x)⁻¹a:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < bn:ℕthis✝³:_fvar.134614 - _fvar.134615 > 0 := ?_mvar.143048this✝²:(_fvar.134614 - _fvar.134615)⁻¹ > 0 := ?_mvar.143475this✝¹:↑_fvar.137254 + (_fvar.134614 - _fvar.134615)⁻¹ > 0 := ?_mvar.145783this✝:(↑_fvar.137254 + (_fvar.134614 - _fvar.134615)⁻¹)⁻¹ > 0 := ?_mvar.148122this:(_fvar.134614 - _fvar.134615)⁻¹ ≤ ↑_fvar.137254 + (_fvar.134614 - _fvar.134615)⁻¹ := ?_mvar.152351⊢ 0 < b - x <;>a:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < bn:ℕthis✝³:_fvar.134614 - _fvar.134615 > 0 := ?_mvar.143048this✝²:(_fvar.134614 - _fvar.134615)⁻¹ > 0 := ?_mvar.143475this✝¹:↑_fvar.137254 + (_fvar.134614 - _fvar.134615)⁻¹ > 0 := ?_mvar.145783this✝:(↑_fvar.137254 + (_fvar.134614 - _fvar.134615)⁻¹)⁻¹ > 0 := ?_mvar.148122this:(_fvar.134614 - _fvar.134615)⁻¹ ≤ ↑_fvar.137254 + (_fvar.134614 - _fvar.134615)⁻¹ := ?_mvar.152351⊢ 0 < ↑n + (b - x)⁻¹a:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < bn:ℕthis✝³:_fvar.134614 - _fvar.134615 > 0 := ?_mvar.143048this✝²:(_fvar.134614 - _fvar.134615)⁻¹ > 0 := ?_mvar.143475this✝¹:↑_fvar.137254 + (_fvar.134614 - _fvar.134615)⁻¹ > 0 := ?_mvar.145783this✝:(↑_fvar.137254 + (_fvar.134614 - _fvar.134615)⁻¹)⁻¹ > 0 := ?_mvar.148122this:(_fvar.134614 - _fvar.134615)⁻¹ ≤ ↑_fvar.137254 + (_fvar.134614 - _fvar.134615)⁻¹ := ?_mvar.152351⊢ 0 < b - x positivityAll goals completed! 🐙
      grindAll goals completed! 🐙
    convert Filter.Tendsto.const_add x (c := 0) _h.e'_1.h.e'_3a:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < b⊢ x = x + 0h.right.convert_4a:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < b⊢ Filter.Tendsto (fun k => 1 / (↑k + (b - x)⁻¹)) Filter.atTop (nhds 0); simph.right.convert_4a:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < b⊢ Filter.Tendsto (fun k => 1 / (↑k + (b - x)⁻¹)) Filter.atTop (nhds 0)
    convert Filter.Tendsto.comp (f := fun (k:ℕ) ↦ (k:ℝ)) (g := fun k ↦ 1/(k+(b-x)⁻¹)) _ tendsto_natCast_atTop_atToph.right.convert_4.convert_2a:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < b⊢ Filter.Tendsto (fun k => 1 / (k + (b - x)⁻¹)) Filter.atTop (nhds 0)
    convert tendsto_mul_add_inv_atTop_nhds_zero 1 (b - x)⁻¹ (bya:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < b⊢ 1 ≠ 0 norm_numAll goals completed! 🐙) using 2 with n; simpAll goals completed! 🐙
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'mem_Ico_isLimit {a b x:ℝ} (hx: x ∈ Set.Ico a b) : LimitPt x (.Ico a b) := bya:ℝb:ℝx:ℝhx:x ∈ Set.Ico a b⊢ LimitPt x (Set.Ico a b)
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'mem_Ioc_isLimit {a b x:ℝ} (hx: x ∈ Set.Ioc a b) : LimitPt x (.Ioc a b) := bya:ℝb:ℝx:ℝhx:x ∈ Set.Ioc a b⊢ LimitPt x (Set.Ioc a b)
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'mem_Ioo_isLimit {a b x:ℝ} (hx: x ∈ Set.Ioo a b) : LimitPt x (.Ioo a b) := bya:ℝb:ℝx:ℝhx:x ∈ Set.Ioo a b⊢ LimitPt x (Set.Ioo a b)
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'mem_Ici_isLimit {a x:ℝ} (hx: x ∈ Set.Ici a) : LimitPt x (.Ici a) := bya:ℝx:ℝhx:x ∈ Set.Ici a⊢ LimitPt x (Set.Ici a)
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'mem_Ioi_isLimit {a x:ℝ} (hx: x ∈ Set.Ioi a) : LimitPt x (.Ioi a) := bya:ℝx:ℝhx:x ∈ Set.Ioi a⊢ LimitPt x (Set.Ioi a)
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'mem_Iic_isLimit {a x:ℝ} (hx: x ∈ Set.Iic a) : LimitPt x (.Iic a) := bya:ℝx:ℝhx:x ∈ Set.Iic a⊢ LimitPt x (Set.Iic a)
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'mem_Iio_isLimit {a x:ℝ} (hx: x ∈ Set.Iio a) : LimitPt x (.Iio a) := bya:ℝx:ℝhx:x ∈ Set.Iio a⊢ LimitPt x (Set.Iio a)
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'mem_R_isLimit {x:ℝ} : LimitPt x (.univ) := byx:ℝ⊢ LimitPt x Set.univ
  sorryAll goals completed! 🐙

Definition 9.1.22. We use here Mathlib's Bornology.IsBounded.{u_2} {α : Type u_2} [Bornology α] (s : Set α) : PropBornology.IsBounded

theorem isBounded_def (X: Set ℝ) : Bornology.IsBounded X ↔ ∃ M > 0, X ⊆ .Icc (-M) M := byX:Set ℝ⊢ Bornology.IsBounded X ↔ ∃ M > 0, X ⊆ Set.Icc (-M) M
  simp [isBounded_iff_forall_norm_le]X:Set ℝ⊢ (∃ C, ∀ x ∈ X, |x| ≤ C) ↔ ∃ M, 0 < M ∧ X ⊆ Set.Icc (-M) M
  constructormpX:Set ℝ⊢ (∃ C, ∀ x ∈ X, |x| ≤ C) → ∃ M, 0 < M ∧ X ⊆ Set.Icc (-M) MmprX:Set ℝ⊢ (∃ M, 0 < M ∧ X ⊆ Set.Icc (-M) M) → ∃ C, ∀ x ∈ X, |x| ≤ C
  .mpX:Set ℝ⊢ (∃ C, ∀ x ∈ X, |x| ≤ C) → ∃ M, 0 < M ∧ X ⊆ Set.Icc (-M) M intro ⟨ C, hC ⟩mpX:Set ℝC:ℝhC:∀ x ∈ X, |x| ≤ C⊢ ∃ M, 0 < M ∧ X ⊆ Set.Icc (-M) M; use (max C 1)hX:Set ℝC:ℝhC:∀ x ∈ X, |x| ≤ C⊢ 0 < max C 1 ∧ X ⊆ Set.Icc (-max C 1) (max C 1)
    refine ⟨ lt_of_lt_of_le (byX:Set ℝC:ℝhC:∀ x ∈ X, |x| ≤ C⊢ 0 < 1 norm_numAll goals completed! 🐙) (le_max_right _ _), ?_ ⟩
    peel hC with x hx hCh.h.hX:Set ℝC:ℝhC✝:∀ x ∈ X, |x| ≤ Cx:ℝhx:x ∈ XhC:|x| ≤ C⊢ x ∈ Set.Icc (-max C 1) (max C 1); rw [abs_le'] at hCh.h.hX:Set ℝC:ℝhC✝:∀ x ∈ X, |x| ≤ Cx:ℝhx:x ∈ XhC:x ≤ C ∧ -x ≤ C⊢ x ∈ Set.Icc (-max C 1) (max C 1); simp [hC.1]h.h.hX:Set ℝC:ℝhC✝:∀ x ∈ X, |x| ≤ Cx:ℝhx:x ∈ XhC:x ≤ C ∧ -x ≤ C⊢ -max C 1 ≤ x; linarith [le_max_left C 1]All goals completed! 🐙
  intro ⟨ M, hM, hXM ⟩mprX:Set ℝM:ℝhM:0 < MhXM:X ⊆ Set.Icc (-M) M⊢ ∃ C, ∀ x ∈ X, |x| ≤ C; use MhX:Set ℝM:ℝhM:0 < MhXM:X ⊆ Set.Icc (-M) M⊢ ∀ x ∈ X, |x| ≤ M; intro x hxhX:Set ℝM:ℝhM:0 < MhXM:X ⊆ Set.Icc (-M) Mx:ℝhx:x ∈ X⊢ |x| ≤ M; specialize hXM hxhX:Set ℝM:ℝhM:0 < Mx:ℝhx:x ∈ XhXM:x ∈ Set.Icc (-M) M⊢ |x| ≤ M; simp_all [abs_le']hX:Set ℝM:ℝhM:0 < Mx:ℝhx:x ∈ XhXM:-M ≤ x ∧ x ≤ M⊢ -x ≤ M; linarith [hXM.1]All goals completed! 🐙

Example 9.1.23

theorem declaration uses 'sorry'Icc_bounded (a b:ℝ) : Bornology.IsBounded (.Icc a b) := bya:ℝb:ℝ⊢ Bornology.IsBounded (Set.Icc a b) sorryAll goals completed! 🐙

Example 9.1.23

theorem declaration uses 'sorry'Ici_unbounded (a: ℝ) : ¬ Bornology.IsBounded (.Ici a) := bya:ℝ⊢ ¬Bornology.IsBounded (Set.Ici a) sorryAll goals completed! 🐙

Example 9.1.23

theorem declaration uses 'sorry'N_unbounded (a: ℝ) : ¬ Bornology.IsBounded ((fun n:ℕ ↦ (n:ℝ)) '' .univ) := bya:ℝ⊢ ¬Bornology.IsBounded ((fun n => ↑n) '' Set.univ) sorryAll goals completed! 🐙

Example 9.1.23

theorem declaration uses 'sorry'Z_unbounded (a: ℝ) : ¬ Bornology.IsBounded ((fun n:ℤ ↦ (n:ℝ)) '' .univ) := bya:ℝ⊢ ¬Bornology.IsBounded ((fun n => ↑n) '' Set.univ) sorryAll goals completed! 🐙

Example 9.1.23

theorem declaration uses 'sorry'Q_unbounded (a: ℝ) : ¬ Bornology.IsBounded ((fun n:ℚ ↦ (n:ℝ)) '' .univ) := bya:ℝ⊢ ¬Bornology.IsBounded ((fun n => ↑n) '' Set.univ) sorryAll goals completed! 🐙

Example 9.1.23

theorem declaration uses 'sorry'R_unbounded (a: ℝ) : ¬ Bornology.IsBounded (.univ: Set ℝ) := bya:ℝ⊢ ¬Bornology.IsBounded Set.univ sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'Heine_Borel (X: Set ℝ) :
  IsClosed X ∧ Bornology.IsBounded X ↔ ∀ a : ℕ → ℝ, (∀ n, a n ∈ X) →
  (∃ n : ℕ → ℕ, StrictMono n
    ∧ ∃ L ∈ X, Filter.atTop.Tendsto (fun j ↦ a (n j)) (nhds L)) := byX: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)
  sorryAll goals completed! 🐙

Exercise 9.1.4

declaration uses 'sorry'example : ∃ (X Y:Set ℝ), closure (X ∩ Y) ≠ closure X ∩ closure Y := byI:Type u_1⊢ ∃ X Y, closure (X ∩ Y) ≠ closure X ∩ closure Y
  sorryAll goals completed! 🐙

Exercise 9.1.6

declaration uses 'sorry'example (X:Set ℝ) : IsClosed (closure X) := byI:Type u_1X:Set ℝ⊢ IsClosed (closure X)
  sorryAll goals completed! 🐙

Exercise 9.1.6

declaration uses 'sorry'example {X Y:Set ℝ} (hY: IsClosed Y) (hXY: X ⊆ Y) : closure X ⊆ Y := byI:Type u_1X:Set ℝY:Set ℝhY:IsClosed YhXY:X ⊆ Y⊢ closure X ⊆ Y
  sorryAll goals completed! 🐙

Exercise 9.1.7

declaration uses 'sorry'example {n:ℕ} (X: Fin n → Set ℝ) (hX: ∀ i, IsClosed (X i)) :
  IsClosed (⋃ i, X i) := byI:Type u_1n:ℕX:Fin n → Set ℝhX:∀ (i : Fin n), IsClosed (X i)⊢ IsClosed (⋃ i, X i)
  sorryAll goals completed! 🐙

Exercise 9.1.8

declaration uses 'sorry'example {I:Type} (X: I → Set ℝ) (hX: ∀ i, IsClosed (X i)) :
  IsClosed (⋂ i, X i) := byI✝:Type u_1I:TypeX:I → Set ℝhX:∀ (i : I), IsClosed (X i)⊢ IsClosed (⋂ i, X i)
  sorryAll goals completed! 🐙

Exercise 9.1.9

declaration uses 'sorry'example {X:Set ℝ} {x:ℝ} (hx: AdherentPt x X) : LimitPt x X ∨ IsolatedPt x X := byI:Type u_1X:Set ℝx:ℝhx:AdherentPt x X⊢ LimitPt x X ∨ IsolatedPt x X
  sorryAll goals completed! 🐙

Exercise 9.1.9

declaration uses 'sorry'example {X:Set ℝ} {x:ℝ} : ¬ (LimitPt x X ∧ IsolatedPt x X) := byI:Type u_1X:Set ℝx:ℝ⊢ ¬(LimitPt x X ∧ IsolatedPt x X)
  sorryAll goals completed! 🐙

Exercise 9.1.10

declaration uses 'sorry'example {X:Set ℝ} (hX: X ≠ ∅) : Bornology.IsBounded X ↔
  sSup ((fun x:ℝ ↦ (x:EReal)) '' X) < ⊤ ∧
  sInf ((fun x:ℝ ↦ (x:EReal)) '' X) > ⊥ := byI:Type u_1X:Set ℝhX:X ≠ ∅⊢ Bornology.IsBounded X ↔ sSup ((fun x => ↑x) '' X) < ⊤ ∧ sInf ((fun x => ↑x) '' X) > ⊥
  sorryAll goals completed! 🐙

Exercise 9.1.11

declaration uses 'sorry'example {X:Set ℝ} (hX: Bornology.IsBounded X) : Bornology.IsBounded (closure X) := byI:Type u_1X:Set ℝhX:Bornology.IsBounded X⊢ Bornology.IsBounded (closure X)
  sorryAll goals completed! 🐙

Exercise 9.1.12. As a followup: prove or disprove this exercise with [Fintype I] : List (Type u_2)[Fintype I] removed.

declaration uses 'sorry'example {I:Type} [Fintype I] (X: I → Set ℝ) (hX: ∀ i, Bornology.IsBounded (X i)) :
  Bornology.IsBounded (⋃ i, X i) := byI✝:Type u_1I:Typeinst✝:Fintype IX:I → Set ℝhX:∀ (i : I), Bornology.IsBounded (X i)⊢ Bornology.IsBounded (⋃ i, X i)
  sorryAll goals completed! 🐙

Exercise 9.1.14

declaration uses 'sorry'example (I: Finset ℝ) : IsClosed (I:Set ℝ) ∧ Bornology.IsBounded (I:Set ℝ) := byI✝:Type u_1I:Finset ℝ⊢ IsClosed ↑I ∧ Bornology.IsBounded ↑I
  sorryAll goals completed! 🐙

Exercise 9.1.15

declaration uses 'sorry'example {E:Set ℝ} (hE: Bornology.IsBounded E) (hnon: E.Nonempty): AdherentPt (sSup E) E ∧ AdherentPt (sSup E) Eᶜ := byI:Type u_1E:Set ℝhE:Bornology.IsBounded Ehnon:E.Nonempty⊢ AdherentPt (sSup E) E ∧ AdherentPt (sSup E) Eᶜ
  sorryAll goals completed! 🐙

end Chapter9