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

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:

Left and right limits

namespace Chapter9

Визначення 9.5.1. We give left and right limits the "junk" value of 0 if the limit does not exist.

abbrev right_limit_exists (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : Prop := ∃ L, Filter.Tendsto f ((nhds x₀) ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds L)

open Classical in
noncomputable abbrev right_limit (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : ℝ := if h : right_limit_exists X f x₀ then h.choose else 0

abbrev left_limit_exists (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : Prop := ∃ L, Filter.Tendsto f ((nhds x₀) ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds L)

open Classical in
noncomputable abbrev left_limit (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : ℝ := if h: left_limit_exists X f x₀ then h.choose else 0

theorem right_limit.eq {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} {L:ℝ} (had: AdherentPt x₀ (X ∩ Set.Ioi x₀))
  (h: Filter.Tendsto f ((nhds x₀) ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds L)) : right_limit X f x₀ = L := byX:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds L)⊢ right_limit X f x₀ = L
  have h' : right_limit_exists X f x₀ := byX:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds L)⊢ right_limit X f x₀ = L use LAll goals completed! 🐙
  simp [right_limit, h']X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds L)h':right_limit_exists X f x₀⊢ Exists.choose ⋯ = L
  have hne : (nhds x₀ ⊓ Filter.principal (X ∩ Set.Ioi x₀)).NeBot := byX:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds L)⊢ right_limit X f x₀ = L
    rwa [←nhdsWithin.eq_1, ←mem_closure_iff_nhdsWithin_neBot, closure_def']X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds L)h':right_limit_exists X f x₀⊢ AdherentPt x₀ (X ∩ Set.Ioi x₀)
  exact tendsto_nhds_unique h'.choose_spec hAll goals completed! 🐙

theorem left_limit.eq {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} {L:ℝ} (had: AdherentPt x₀ (X ∩ Set.Iio x₀)) (h: Filter.Tendsto f ((nhds x₀) ⊓ Filter.principal (X ∩ Set.Iio x₀))
  (nhds L)) : left_limit X f x₀ = L := byX:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds L)⊢ left_limit X f x₀ = L
  have h' : left_limit_exists X f x₀ := byX:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds L)⊢ left_limit X f x₀ = L use LAll goals completed! 🐙
  simp [left_limit, h']X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds L)h':left_limit_exists X f x₀⊢ Exists.choose ⋯ = L
  have hne : (nhds x₀ ⊓ Filter.principal (X ∩ Set.Iio x₀)).NeBot := byX:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds L)⊢ left_limit X f x₀ = L
    rwa [←nhdsWithin.eq_1, ←mem_closure_iff_nhdsWithin_neBot, closure_def']X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds L)h':left_limit_exists X f x₀⊢ AdherentPt x₀ (X ∩ Set.Iio x₀)
  exact tendsto_nhds_unique h'.choose_spec hAll goals completed! 🐙

theorem right_limit.eq' {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (h: right_limit_exists X f x₀) : Filter.Tendsto f ((nhds x₀) ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds (right_limit X f x₀)) := byX:Set ℝf:ℝ → ℝx₀:ℝh:right_limit_exists X f x₀⊢ Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds (right_limit X f x₀))
    simp [right_limit, h]X:Set ℝf:ℝ → ℝx₀:ℝh:right_limit_exists X f x₀⊢ Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds (Exists.choose ⋯))
    convert h.choose_specAll goals completed! 🐙

theorem left_limit.eq' {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (h: left_limit_exists X f x₀) : Filter.Tendsto f ((nhds x₀) ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds (left_limit X f x₀)) := byX:Set ℝf:ℝ → ℝx₀:ℝh:left_limit_exists X f x₀⊢ Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds (left_limit X f x₀))
  simp [left_limit, h]X:Set ℝf:ℝ → ℝx₀:ℝh:left_limit_exists X f x₀⊢ Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds (Exists.choose ⋯))
  convert h.choose_specAll goals completed! 🐙

Приклад 9.5.2. The second part of this example is no longer operative as we assign "junk" values to our functions instead of leaving them undefined.

declaration uses 'sorry'example : right_limit Set.univ Real.sign 0 = 1 := by⊢ right_limit Set.univ Real.sign 0 = 1 sorryAll goals completed! 🐙

declaration uses 'sorry'example : left_limit Set.univ Real.sign 0 = -1 := by⊢ left_limit Set.univ Real.sign 0 = -1 sorryAll goals completed! 🐙

theorem right_limit.conv {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} {unused variable `L`
note: this linter can be disabled with `set_option linter.unusedVariables false`L:ℝ} (had: AdherentPt x₀ (X ∩ Set.Ioi x₀))
  (h: right_limit_exists X f x₀)
  (a:ℕ → ℝ) (ha: ∀ n, a n ∈ X ∩ Set.Ioi x₀)
  (hconv: Filter.Tendsto a Filter.atTop (nhds x₀)) :
  Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds (right_limit X f x₀)) := byX:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:right_limit_exists X f x₀a:ℕ → ℝha:∀ (n : ℕ), a n ∈ X ∩ Set.Ioi x₀hconv:Filter.Tendsto a Filter.atTop (nhds x₀)⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (right_limit X f x₀))
  obtain ⟨ L, hL ⟩ := hintroX:Set ℝf:ℝ → ℝx₀:ℝL✝:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ X ∩ Set.Ioi x₀hconv:Filter.Tendsto a Filter.atTop (nhds x₀)L:ℝhL:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds L)⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (right_limit X f x₀))
  apply Convergesto.comp had _ ha hconvX:Set ℝf:ℝ → ℝx₀:ℝL✝:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ X ∩ Set.Ioi x₀hconv:Filter.Tendsto a Filter.atTop (nhds x₀)L:ℝhL:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds L)⊢ Convergesto (X ∩ Set.Ioi x₀) f (right_limit X f x₀) x₀
  rwa [Convergesto.iff, right_limit.eq had hL]X:Set ℝf:ℝ → ℝx₀:ℝL✝:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ X ∩ Set.Ioi x₀hconv:Filter.Tendsto a Filter.atTop (nhds x₀)L:ℝhL:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds L)⊢ Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds L)

theorem left_limit.conv {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} {unused variable `L`
note: this linter can be disabled with `set_option linter.unusedVariables false`L:ℝ} (had: AdherentPt x₀ (X ∩ Set.Iio x₀))
  (h: left_limit_exists X f x₀)
  (a:ℕ → ℝ) (ha: ∀ n, a n ∈ X ∩ Set.Iio x₀)
  (hconv: Filter.Tendsto a Filter.atTop (nhds x₀)) :
  Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds (left_limit X f x₀)) := byX:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:left_limit_exists X f x₀a:ℕ → ℝha:∀ (n : ℕ), a n ∈ X ∩ Set.Iio x₀hconv:Filter.Tendsto a Filter.atTop (nhds x₀)⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (left_limit X f x₀))
  obtain ⟨ L, hL ⟩ := hintroX:Set ℝf:ℝ → ℝx₀:ℝL✝:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ X ∩ Set.Iio x₀hconv:Filter.Tendsto a Filter.atTop (nhds x₀)L:ℝhL:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds L)⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (left_limit X f x₀))
  apply Convergesto.comp had _ ha hconvX:Set ℝf:ℝ → ℝx₀:ℝL✝:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ X ∩ Set.Iio x₀hconv:Filter.Tendsto a Filter.atTop (nhds x₀)L:ℝhL:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds L)⊢ Convergesto (X ∩ Set.Iio x₀) f (left_limit X f x₀) x₀
  rwa [Convergesto.iff, left_limit.eq had hL]X:Set ℝf:ℝ → ℝx₀:ℝL✝:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ X ∩ Set.Iio x₀hconv:Filter.Tendsto a Filter.atTop (nhds x₀)L:ℝhL:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds L)⊢ Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds L)

Твердження 9.5.3

theorem declaration uses 'sorry'ContinuousAt.iff_eq_left_right_limit {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (h: x₀ ∈ X)
  (had_left: AdherentPt x₀ (X ∩ Set.Iio x₀)) (had_right: AdherentPt x₀ (X ∩ Set.Ioi x₀)) :
  ContinuousWithinAt f X x₀ ↔ right_limit_exists X f x₀ ∧ left_limit_exists X f x₀ ∧
  right_limit X f x₀ = f x₀ ∧ left_limit X f x₀ = f x₀ := byX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)⊢ ContinuousWithinAt f X x₀ ↔
  right_limit_exists X f x₀ ∧ left_limit_exists X f x₀ ∧ right_limit X f x₀ = f x₀ ∧ left_limit X f x₀ = f x₀
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  constructormpX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)⊢ ContinuousWithinAt f X x₀ →
  right_limit_exists X f x₀ ∧ left_limit_exists X f x₀ ∧ right_limit X f x₀ = f x₀ ∧ left_limit X f x₀ = f x₀mprX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)⊢ right_limit_exists X f x₀ ∧ left_limit_exists X f x₀ ∧ right_limit X f x₀ = f x₀ ∧ left_limit X f x₀ = f x₀ →
  ContinuousWithinAt f X x₀
  .mpX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)⊢ ContinuousWithinAt f X x₀ →
  right_limit_exists X f x₀ ∧ left_limit_exists X f x₀ ∧ right_limit X f x₀ = f x₀ ∧ left_limit X f x₀ = f x₀ sorryAll goals completed! 🐙
  rintro ⟨ hre, hle, hright, lheft ⟩mpr.intro.intro.introX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)hre:right_limit_exists X f x₀hle:left_limit_exists X f x₀hright:right_limit X f x₀ = f x₀lheft:left_limit X f x₀ = f x₀⊢ ContinuousWithinAt f X x₀
  set L := f x₀mpr.intro.intro.introX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)hre:right_limit_exists X f x₀hle:left_limit_exists X f x₀L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = L⊢ ContinuousWithinAt f X x₀
  have := (ContinuousWithinAt.tfae X f h).out 0 2mpr.intro.intro.introX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)hre:right_limit_exists X f x₀hle:left_limit_exists X f x₀L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε⊢ ContinuousWithinAt f X x₀
  rw [this]mpr.intro.intro.introX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)hre:right_limit_exists X f x₀hle:left_limit_exists X f x₀L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε⊢ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε
  intro ε hεmpr.intro.intro.introX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)hre:right_limit_exists X f x₀hle:left_limit_exists X f x₀L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0⊢ ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε
  replace hre := right_limit.eq' hrempr.intro.intro.introX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)hle:left_limit_exists X f x₀L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0hre:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds (right_limit X f x₀))⊢ ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε
  replace hle := left_limit.eq' hlempr.intro.intro.introX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0hre:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds (right_limit X f x₀))hle:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds (left_limit X f x₀))⊢ ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε
  rw [hright, ←Convergesto.iff] at hrempr.intro.intro.introX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0hre:Convergesto (X ∩ Set.Ioi x₀) f L x₀hle:Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds (left_limit X f x₀))⊢ ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε
  rw [lheft, ←Convergesto.iff] at hlempr.intro.intro.introX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0hre:Convergesto (X ∩ Set.Ioi x₀) f L x₀hle:Convergesto (X ∩ Set.Iio x₀) f L x₀⊢ ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε
  simp [Convergesto, Real.close_near, Real.close_fn] at hre hlempr.intro.intro.introX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0hre:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ < x → x₀ - δ < x → x < x₀ + δ → |f x - L| < εhle:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ x ∈ X, x < x₀ → x₀ - δ < x → x < x₀ + δ → |f x - L| < ε⊢ ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε
  specialize hre ε hεmpr.intro.intro.introX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0hle:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ x ∈ X, x < x₀ → x₀ - δ < x → x < x₀ + δ → |f x - L| < εhre:∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ < x → x₀ - δ < x → x < x₀ + δ → |f x - L| < ε⊢ ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε
  specialize hle ε hεmpr.intro.intro.introX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0hre:∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ < x → x₀ - δ < x → x < x₀ + δ → |f x - L| < εhle:∃ δ, 0 < δ ∧ ∀ x ∈ X, x < x₀ → x₀ - δ < x → x < x₀ + δ → |f x - L| < ε⊢ ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε
  obtain ⟨ δ_plus, hδ_plus, hre ⟩ := hrempr.intro.intro.intro.intro.introX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0hle:∃ δ, 0 < δ ∧ ∀ x ∈ X, x < x₀ → x₀ - δ < x → x < x₀ + δ → |f x - L| < εδ_plus:ℝhδ_plus:0 < δ_plushre:∀ x ∈ X, x₀ < x → x₀ - δ_plus < x → x < x₀ + δ_plus → |f x - L| < ε⊢ ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε
  obtain ⟨ δ_minus, hδ_minus, hle ⟩ := hlempr.intro.intro.intro.intro.intro.intro.introX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ_plus:ℝhδ_plus:0 < δ_plushre:∀ x ∈ X, x₀ < x → x₀ - δ_plus < x → x < x₀ + δ_plus → |f x - L| < εδ_minus:ℝhδ_minus:0 < δ_minushle:∀ x ∈ X, x < x₀ → x₀ - δ_minus < x → x < x₀ + δ_minus → |f x - L| < ε⊢ ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε
  use min δ_plus δ_minus, (byX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ_plus:ℝhδ_plus:0 < δ_plushre:∀ x ∈ X, x₀ < x → x₀ - δ_plus < x → x < x₀ + δ_plus → |f x - L| < εδ_minus:ℝhδ_minus:0 < δ_minushle:∀ x ∈ X, x < x₀ → x₀ - δ_minus < x → x < x₀ + δ_minus → |f x - L| < ε⊢ min δ_plus δ_minus > 0 positivityAll goals completed! 🐙)
  intro x hx hxx₀rightX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ_plus:ℝhδ_plus:0 < δ_plushre:∀ x ∈ X, x₀ < x → x₀ - δ_plus < x → x < x₀ + δ_plus → |f x - L| < εδ_minus:ℝhδ_minus:0 < δ_minushle:∀ x ∈ X, x < x₀ → x₀ - δ_minus < x → x < x₀ + δ_minus → |f x - L| < εx:ℝhx:x ∈ Xhxx₀:|x - x₀| < min δ_plus δ_minus⊢ |f x - f x₀| < ε
  rcases lt_trichotomy x x₀ with hlt | heq | hgtright.inlX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ_plus:ℝhδ_plus:0 < δ_plushre:∀ x ∈ X, x₀ < x → x₀ - δ_plus < x → x < x₀ + δ_plus → |f x - L| < εδ_minus:ℝhδ_minus:0 < δ_minushle:∀ x ∈ X, x < x₀ → x₀ - δ_minus < x → x < x₀ + δ_minus → |f x - L| < εx:ℝhx:x ∈ Xhxx₀:|x - x₀| < min δ_plus δ_minushlt:x < x₀⊢ |f x - f x₀| < εright.inr.inlX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ_plus:ℝhδ_plus:0 < δ_plushre:∀ x ∈ X, x₀ < x → x₀ - δ_plus < x → x < x₀ + δ_plus → |f x - L| < εδ_minus:ℝhδ_minus:0 < δ_minushle:∀ x ∈ X, x < x₀ → x₀ - δ_minus < x → x < x₀ + δ_minus → |f x - L| < εx:ℝhx:x ∈ Xhxx₀:|x - x₀| < min δ_plus δ_minusheq:x = x₀⊢ |f x - f x₀| < εright.inr.inrX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ_plus:ℝhδ_plus:0 < δ_plushre:∀ x ∈ X, x₀ < x → x₀ - δ_plus < x → x < x₀ + δ_plus → |f x - L| < εδ_minus:ℝhδ_minus:0 < δ_minushle:∀ x ∈ X, x < x₀ → x₀ - δ_minus < x → x < x₀ + δ_minus → |f x - L| < εx:ℝhx:x ∈ Xhxx₀:|x - x₀| < min δ_plus δ_minushgt:x₀ < x⊢ |f x - f x₀| < ε
  .right.inlX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ_plus:ℝhδ_plus:0 < δ_plushre:∀ x ∈ X, x₀ < x → x₀ - δ_plus < x → x < x₀ + δ_plus → |f x - L| < εδ_minus:ℝhδ_minus:0 < δ_minushle:∀ x ∈ X, x < x₀ → x₀ - δ_minus < x → x < x₀ + δ_minus → |f x - L| < εx:ℝhx:x ∈ Xhxx₀:|x - x₀| < min δ_plus δ_minushlt:x < x₀⊢ |f x - f x₀| < ε sorryAll goals completed! 🐙
  .right.inr.inlX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := f x₀hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt f X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ_plus:ℝhδ_plus:0 < δ_plushre:∀ x ∈ X, x₀ < x → x₀ - δ_plus < x → x < x₀ + δ_plus → |f x - L| < εδ_minus:ℝhδ_minus:0 < δ_minushle:∀ x ∈ X, x < x₀ → x₀ - δ_minus < x → x < x₀ + δ_minus → |f x - L| < εx:ℝhx:x ∈ Xhxx₀:|x - x₀| < min δ_plus δ_minusheq:x = x₀⊢ |f x - f x₀| < ε sorryAll goals completed! 🐙
  sorryAll goals completed! 🐙

abbrev has_jump_discontinuity (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : Prop :=
  right_limit_exists X f x₀ ∧ left_limit_exists X f x₀ ∧ right_limit X f x₀ ≠ left_limit X f x₀

declaration uses 'sorry'example : has_jump_discontinuity Set.univ Real.sign 0 := by⊢ has_jump_discontinuity Set.univ Real.sign 0 sorryAll goals completed! 🐙

abbrev has_removable_discontinuity (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : Prop :=
  right_limit_exists X f x₀ ∧ left_limit_exists X f x₀ ∧ right_limit X f x₀ = left_limit X f x₀ ∧
  right_limit X f x₀ ≠ f x₀

declaration uses 'sorry'example : has_removable_discontinuity Set.univ f_9_3_17 0 := by⊢ has_removable_discontinuity Set.univ f_9_3_17 0 sorryAll goals completed! 🐙

declaration uses 'sorry'example : ¬ has_removable_discontinuity Set.univ (fun x ↦ 1/x) 0 := by⊢ ¬has_removable_discontinuity Set.univ (fun x => 1 / x) 0 sorryAll goals completed! 🐙

declaration uses 'sorry'example : ¬ has_jump_discontinuity Set.univ (fun x ↦ 1/x) 0 := by⊢ ¬has_jump_discontinuity Set.univ (fun x => 1 / x) 0 sorryAll goals completed! 🐙

/- Вправа 9.5.1: Write down a definition of what it would mean for a limit of a function to be `+∞` or `-∞`, apply to `fun x ↦ 1/x`, and state and prove a version of Proposition 9.3.9. -/


end Chapter9