Аналіз I, Глава 9.1

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:

Intervals
Adherent points, limit points, isolated points
Closed sets and closure
The Heine-Borel theorem for the real line

/- Definition 9.1.1 (Intervals) -/
Set.Icc_def.{u_1} {α : Type u_1} [Preorder α] (a b : α) : {x | a ≤ x ∧ x ≤ b} = Set.Icc a b#check Set.Icc_def

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#check Set.Ico_def

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#check Set.Ioc_def

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#check Set.Ioo_def

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#check Set.Ici_def

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#check Set.Ioi_def

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#check Set.Iic_def

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#check Set.Iio_def

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#check EReal.image_coe_Icc

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#check EReal.image_coe_Ico

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#check EReal.image_coe_Ioc

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#check EReal.image_coe_Ioo

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 ⊤#check EReal.image_coe_Ici

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 ⊤#check EReal.image_coe_Ioi

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#check EReal.image_coe_Iic

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#check EReal.image_coe_Iio

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

Приклад 9.1.4

declaration uses 'sorry'example {a b: EReal} (h: a > b) : Set.Icc a b = ∅ := bya: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 = ∅ := bya: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 = ∅ := bya: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 = ∅ := bya: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} := bya:ERealb:ERealh:a = b⊢ Set.Icc a a = {a}
  sorryAll goals completed! 🐙

Визначення 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| ≤ ε

Приклад 9.1.7

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

declaration uses 'sorry'example : ¬ (0.1:ℝ).adherent' 1.1 (Set.Ioo 0 1) := by⊢ ¬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} := by⊢ Real.adherent' 0.5 1.1 {1, 2, 3} sorryAll goals completed! 🐙

namespace Chapter9

Визначення 9.1.

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

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

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

Визначення 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}
  ext xhX: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| ≤ ε intro h ε hεh.mpX:Set ℝx:ℝh:∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |y - x| < εε:ℝhε:0 < ε⊢ ∃ y ∈ X, |x - y| ≤ ε
    obtain ⟨ y, hy, hxy ⟩ := h ε hεh.mp.intro.introX:Set ℝx:ℝh:∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |y - x| < εε:ℝhε:0 < εy:ℝhy:y ∈ Xhxy:|y - x| < ε⊢ ∃ y ∈ X, |x - y| ≤ ε
    refine ⟨ y, hy, ?_ ⟩h.mp.intro.introX:Set ℝx:ℝh:∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |y - x| < εε:ℝhε:0 < εy:ℝhy:y ∈ Xhxy:|y - x| < ε⊢ |x - y| ≤ ε
    rw [abs_sub_comm]h.mp.intro.introX:Set ℝx:ℝh:∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |y - x| < εε:ℝhε:0 < εy:ℝhy:y ∈ Xhxy:|y - x| < ε⊢ |y - x| ≤ ε; linarithAll goals completed! 🐙
  intro h ε hεh.mprX:Set ℝx:ℝh:∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |x - y| ≤ εε:ℝhε:0 < ε⊢ ∃ y ∈ X, |y - x| < ε
  obtain ⟨ y, hy, hxy ⟩ := h (ε/2) (half_pos hε)h.mpr.intro.introX:Set ℝx:ℝh:∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |x - y| ≤ εε:ℝhε:0 < εy:ℝhy:y ∈ Xhxy:|x - y| ≤ ε / 2⊢ ∃ y ∈ X, |y - x| < ε
  refine ⟨ y, hy, ?_ ⟩h.mpr.intro.introX:Set ℝx:ℝh:∀ (ε : ℝ), 0 < ε → ∃ y ∈ X, |x - y| ≤ εε:ℝhε:0 < εy:ℝhy:y ∈ Xhxy:|x - y| ≤ ε / 2⊢ |y - x| < ε
  rw [abs_sub_comm]h.mpr.intro.introX: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 unknown identifier 'AdherentPt'AdherentPt 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 (Filter.principal X) := byx:ℝX:Set ℝ⊢ AdherentPt x X = ClusterPt x (Filter.principal X)
  rw [←closure_def', mem_closure_iff_clusterPt]All goals completed! 🐙

Лема 9.1.11 / Вправа 9.1.2

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

Лема 9.1.11 / Вправа 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! 🐙

Лема 9.1.11 / Вправа 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! 🐙

Лема 9.1.11 / Вправа 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! 🐙

Вправа 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! 🐙

Лема 9.1.12

theorem declaration uses 'sorry'closure_of_Ioo {a b:ℝ} (h:a < b) : closure (Set.Ioo a b) = Set.Icc a b := bya:ℝb:ℝh:a < b⊢ closure (Set.Ioo a b) = Set.Icc a b
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  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|
    rcases le_or_gt a x with h' | h'h.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':a > x⊢ ∃ ε, 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! 🐙
      rintro y ⟨ h1, h2 ⟩right.introa:ℝb:ℝh✝:a < bx:ℝh':a ≤ xh:b < xy:ℝh1:a < yh2:y < b⊢ x - b < |x - y|
      apply lt_of_lt_of_le _ (le_abs_self _)a:ℝb:ℝh✝:a < bx:ℝh':a ≤ xh:b < xy:ℝh1:a < yh2:y < b⊢ x - b < x - y
      linarithAll goals completed! 🐙
    use a-x, bya:ℝb:ℝh✝:a < bx:ℝh:a ≤ x → b < xh':a > x⊢ 0 < a - x linarithAll goals completed! 🐙
    rintro y ⟨ h1, h2 ⟩right.introa:ℝb:ℝh✝:a < bx:ℝh:a ≤ x → b < xh':a > xy:ℝh1:a < yh2:y < b⊢ a - x < |x - y|
    apply lt_of_lt_of_le _ (neg_le_abs _)a:ℝb:ℝh✝:a < bx:ℝh:a ≤ x → b < xh':a > xy:ℝh1:a < yh2:y < b⊢ a - x < -(x - y)
    linarithAll goals completed! 🐙
  rintro ⟨ h1, h2 ⟩h.mpr.introa:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ b⊢ ∀ (ε : ℝ), 0 < ε → ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ ε
  by_cases ha : x = aposa:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bha:x = a⊢ ∀ (ε : ℝ), 0 < ε → ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ εnega:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bha:¬x = a⊢ ∀ (ε : ℝ), 0 < ε → ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ ε
  .posa:ℝ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 = bposa:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bha:¬x = ahb:x = b⊢ ∀ (ε : ℝ), 0 < ε → ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ εnega:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bha:¬x = ahb:¬x = b⊢ ∀ (ε : ℝ), 0 < ε → ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ ε
  .posa:ℝ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 ε hεnega:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bha:¬x = ahb:¬x = bε:ℝhε:0 < ε⊢ ∃ y, (a < y ∧ y < b) ∧ |x - y| ≤ ε
  use x, ⟨ bya:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bha:¬x = ahb:¬x = bε:ℝhε:0 < ε⊢ a < x contrapose! haa:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bhb:¬x = bε:ℝhε:0 < εha:x ≤ a⊢ x = a; linarithAll goals completed! 🐙, bya:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bha:¬x = ahb:¬x = bε:ℝhε:0 < ε⊢ x < b contrapose! hba:ℝb:ℝh:a < bx:ℝh1:a ≤ xh2:x ≤ bha:¬x = aε:ℝhε:0 < εhb:b ≤ x⊢ x = b; linarithAll goals completed! 🐙 ⟩
  simp [le_of_lt hε]All goals completed! 🐙

theorem declaration uses 'sorry'closure_of_Ioc {a b:ℝ} (h:a < b) : closure (Set.Ioc a b) = Set.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 (Set.Ico a b) = Set.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 (Set.Icc a b) = Set.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 (Set.Ioi a) = Set.Ici a := bya:ℝ⊢ closure (Set.Ioi a) = Set.Ici a
  sorryAll goals completed! 🐙

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

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

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

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

Лема 9.1.13 / Вправа 9.1.3

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

Лема 9.1.13 / Вправа 9.1.3

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

Лема 9.1.13 / Вправа 9.1.3

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

Лема 9.1.14 / Вправа 9.1.5

theorem declaration uses 'sorry'limit_of_AdherentPt (X: Set ℝ) (x:ℝ) :
  AdherentPt x X ↔ ∃ a : ℕ → ℝ, (∀ n, a n ∈ X) ∧ Filter.Tendsto a Filter.atTop (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! 🐙

Визначення 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! 🐙

Приклади 9.1.16

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

Приклади 9.1.16

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

Приклади 9.1.16

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

Приклади 9.1.16

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

Приклади 9.1.16

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

Приклади 9.1.16

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

Приклади 9.1.16

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

Приклади 9.1.16

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

Приклади 9.1.16

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

Приклади 9.1.16

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

Приклади 9.1.16

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

Приклади 9.1.16

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

Наслідок 9.1.17

theorem isClosed_iff_limits_mem (X: Set ℝ) :
  IsClosed X ↔ ∀ (a:ℕ → ℝ) (L:ℝ), (∀ n, a n ∈ X) → Filter.Tendsto a Filter.atTop (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 a L ha hLmpX:Set ℝh:∀ (x : ℝ), AdherentPt x X → x ∈ Xa:ℕ → ℝL:ℝha:∀ (n : ℕ), a n ∈ XhL:Filter.Tendsto a Filter.atTop (nhds L)⊢ L ∈ X
    apply h LmpX:Set ℝh:∀ (x : ℝ), AdherentPt x X → x ∈ Xa:ℕ → ℝL:ℝha:∀ (n : ℕ), a n ∈ XhL:Filter.Tendsto a Filter.atTop (nhds L)⊢ AdherentPt L X
    rw [limit_of_AdherentPt]mpX:Set ℝh:∀ (x : ℝ), AdherentPt x X → x ∈ Xa:ℕ → ℝL:ℝha:∀ (n : ℕ), a n ∈ XhL:Filter.Tendsto a Filter.atTop (nhds L)⊢ ∃ a, (∀ (n : ℕ), a n ∈ X) ∧ Filter.Tendsto a Filter.atTop (nhds L)
    exact ⟨a, ha, hL ⟩All goals completed! 🐙
  intro h x hxmprX:Set ℝh:∀ (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 ℝh:∀ (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
  obtain ⟨ a, ha, hL ⟩ := hxmpr.intro.introX:Set ℝh:∀ (a : ℕ → ℝ) (L : ℝ), (∀ (n : ℕ), a n ∈ X) → Filter.Tendsto a Filter.atTop (nhds L) → L ∈ Xx:ℝa:ℕ → ℝha:∀ (n : ℕ), a n ∈ XhL:Filter.Tendsto a Filter.atTop (nhds x)⊢ x ∈ X
  exact h a x ha hLAll goals completed! 🐙

Визначення 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 (Filter.principal X) := byx:ℝX:Set ℝ⊢ LimitPt x X ↔ AccPt x (Filter.principal X)
  rw [accPt_principal_iff_clusterPt,←AdherentPt_def]All goals completed! 🐙

Визначення 9.1.18 (Isolated points)

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

Приклад 9.1.19

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

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

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

Ремарка 9.1.20

theorem LimitPt.iff_limit (x:ℝ) (X: Set ℝ) :
  LimitPt x X ↔ ∃ a : ℕ → ℝ, (∀ n, a n ∈ X \ {x}) ∧ Filter.Tendsto a Filter.atTop (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! 🐙

open Filter in
/-- This lemma is in more recent versions of Mathlib and can be deleted once Mathlib is updated. -/
theorem tendsto_mul_add_inv_atTop_nhds_zero (a c : ℝ) (ha : a ≠ 0) :
    Tendsto (fun x => (a * x + c)⁻¹) atTop (nhds 0) := bya:ℝc:ℝha:a ≠ 0⊢ Tendsto (fun x => (a * x + c)⁻¹) atTop (nhds 0)
  obtain ha' | ha' := lt_or_gt_of_ne hainla:ℝc:ℝha:a ≠ 0ha':a < 0⊢ Tendsto (fun x => (a * x + c)⁻¹) atTop (nhds 0)inra:ℝc:ℝha:a ≠ 0ha':a > 0⊢ Tendsto (fun x => (a * x + c)⁻¹) atTop (nhds 0)
  ·inla:ℝc:ℝha:a ≠ 0ha':a < 0⊢ Tendsto (fun x => (a * x + c)⁻¹) atTop (nhds 0) exact tendsto_inv_atBot_zero.comp
      (tendsto_atBot_add_const_right _ c (tendsto_id.const_mul_atTop_of_neg ha'))All goals completed! 🐙
  ·inra:ℝc:ℝha:a ≠ 0ha':a > 0⊢ Tendsto (fun x => (a * x + c)⁻¹) atTop (nhds 0) exact tendsto_inv_atTop_zero.comp
      (tendsto_atTop_add_const_right _ c (tendsto_id.const_mul_atTop ha'))All goals completed! 🐙

Лема 9.1.21

theorem declaration uses 'sorry'mem_Icc_isLimit {a b x:ℝ} (h: a < b) (hx: x ∈ Set.Icc a b) : LimitPt x (Set.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)
  rcases le_iff_lt_or_eq.1 hx.2 with hxb | hxbinla:ℝ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! 🐙
      refine ⟨ ⟨ ?_, ?_⟩, bya:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < bn:ℕthis✝¹:b - x > 0this✝:(b - x)⁻¹ > 0this:↑n + (b - x)⁻¹ > 0⊢ ¬↑n + (b - x)⁻¹ = 0 linarithAll goals completed! 🐙 ⟩
      .h.left.refine_1a:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < bn:ℕthis✝¹:b - x > 0this✝:(b - x)⁻¹ > 0this:↑n + (b - x)⁻¹ > 0⊢ a ≤ x + (↑n + (b - x)⁻¹)⁻¹ 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! 🐙
        linarithAll 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₀ (bya:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < bn:ℕthis✝²:b - x > 0this✝¹:(b - x)⁻¹ > 0this✝:↑n + (b - x)⁻¹ > 0this:(b - x)⁻¹ ≤ ↑n + (b - x)⁻¹⊢ 0 < ↑n + (b - x)⁻¹ positivityAll goals completed! 🐙) (bya:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < bn:ℕthis✝²:b - x > 0this✝¹:(b - x)⁻¹ > 0this✝:↑n + (b - x)⁻¹ > 0this:(b - x)⁻¹ ≤ ↑n + (b - x)⁻¹⊢ 0 < b - x positivityAll goals completed! 🐙)]a:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < bn:ℕthis✝²:b - x > 0this✝¹:(b - x)⁻¹ > 0this✝:↑n + (b - x)⁻¹ > 0this:(b - x)⁻¹ ≤ ↑n + (b - x)⁻¹⊢ (b - x)⁻¹ ≤ ↑n + (b - x)⁻¹
      linarithAll 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)
    .h.e'_1.h.e'_3a:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < b⊢ x = x + 0 simpAll goals completed! 🐙
    convert Filter.Tendsto.comp (f := fun (k:ℕ) ↦ (k:ℝ)) (g := fun k ↦ 1/(k+(b-x)⁻¹)) (y := Filter.atTop) _ _h.right.convert_4.convert_3a:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < b⊢ Filter.Tendsto (fun k => 1 / (k + (b - x)⁻¹)) Filter.atTop (nhds 0)h.right.convert_4.convert_4a:ℝb:ℝx:ℝh:a < bhx:a ≤ x ∧ x ≤ bhxb:x < b⊢ Filter.Tendsto (fun k => ↑k) Filter.atTop Filter.atTop
    .h.right.convert_4.convert_3a:ℝ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! 🐙
    exact tendsto_natCast_atTop_atTopAll goals completed! 🐙
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'mem_Ico_isLimit {a b x:ℝ} (hx: x ∈ Set.Ico a b) : LimitPt x (Set.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 (Set.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 (Set.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 (Set.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 (Set.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 (Set.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 (Set.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 (Set.univ) := byx:ℝ⊢ LimitPt x Set.univ
  sorryAll goals completed! 🐙

Визначення 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 ⊆ Set.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 hmpX:Set ℝh:∃ C, ∀ x ∈ X, |x| ≤ C⊢ ∃ M, 0 < M ∧ X ⊆ Set.Icc (-M) M
    obtain ⟨ C, hC ⟩ := hmp.introX: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)
    constructorh.leftX:Set ℝC:ℝhC:∀ x ∈ X, |x| ≤ C⊢ 0 < max C 1h.rightX:Set ℝC:ℝhC:∀ x ∈ X, |x| ≤ C⊢ X ⊆ Set.Icc (-max C 1) (max C 1)
    .h.leftX:Set ℝC:ℝhC:∀ x ∈ X, |x| ≤ C⊢ 0 < max C 1 apply lt_of_lt_of_le _ (le_max_right _ _)X:Set ℝC:ℝhC:∀ x ∈ X, |x| ≤ C⊢ 0 < 1
      norm_numAll goals completed! 🐙
    intro x hxh.rightX:Set ℝC:ℝhC:∀ x ∈ X, |x| ≤ Cx:ℝhx:x ∈ X⊢ x ∈ Set.Icc (-max C 1) (max C 1)
    specialize hC x hxh.rightX:Set ℝC:ℝx:ℝhx:x ∈ XhC:|x| ≤ C⊢ x ∈ Set.Icc (-max C 1) (max C 1)
    rw [abs_le'] at hCh.rightX:Set ℝC:ℝx:ℝhx:x ∈ XhC:x ≤ C ∧ -x ≤ C⊢ x ∈ Set.Icc (-max C 1) (max C 1)
    simp [hC.1, hC.2]h.rightX:Set ℝC:ℝx:ℝhx:x ∈ XhC:x ≤ C ∧ -x ≤ C⊢ -max C 1 ≤ x
    have := le_max_left C 1h.rightX:Set ℝC:ℝx:ℝhx:x ∈ XhC:x ≤ C ∧ -x ≤ Cthis:C ≤ max C 1⊢ -max C 1 ≤ x
    linarithAll goals completed! 🐙
  intro hmprX:Set ℝh:∃ M, 0 < M ∧ X ⊆ Set.Icc (-M) M⊢ ∃ C, ∀ x ∈ X, |x| ≤ C
  obtain ⟨ M, hM, hXM ⟩ := hmpr.intro.introX: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
  replace hXM := hXM hxhX:Set ℝM:ℝhM:0 < Mx:ℝhx:x ∈ XhXM:x ∈ Set.Icc (-M) M⊢ |x| ≤ M
  simp [abs_le'] at hXM ⊢hX:Set ℝM:ℝhM:0 < Mx:ℝhx:x ∈ XhXM:-M ≤ x ∧ x ≤ M⊢ x ≤ M ∧ -x ≤ M
  simp [hXM]hX:Set ℝM:ℝhM:0 < Mx:ℝhx:x ∈ XhXM:-M ≤ x ∧ x ≤ M⊢ -x ≤ M
  linarith [hXM.1]All goals completed! 🐙

Приклад 9.1.23

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

Приклад 9.1.23

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

Приклад 9.1.23

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

Приклад 9.1.23

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

Приклад 9.1.23

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

Приклад 9.1.23

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

Теорема 9.1.24 / Вправа 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.Tendsto (fun j ↦ a (n j)) Filter.atTop (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! 🐙

Вправа 9.1.4

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

Вправа 9.1.6

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

Вправа 9.1.6

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

Вправа 9.1.7

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

Вправа 9.1.8

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

Вправа 9.1.9

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

Вправа 9.1.9

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

Вправа 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) > ⊥ := byX:Set ℝhX:X ≠ ∅⊢ Bornology.IsBounded X ↔ sSup ((fun x => ↑x) '' X) < ⊤ ∧ sInf ((fun x => ↑x) '' X) > ⊥
  sorryAll goals completed! 🐙

Вправа 9.1.11

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

Вправа 9.1.12. As a followup: prove or disprove this exercise with [Fintype sorry] : List (Type u_1)[Fintype unknown identifier 'I'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:Typeinst✝:Fintype IX:I → Set ℝhX:∀ (i : I), Bornology.IsBounded (X i)⊢ Bornology.IsBounded (⋃ i, X i)
  sorryAll goals completed! 🐙

Вправа 9.1.14

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

Вправа 9.1.15

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

end Chapter9