Analysis I, Section 9.5: Left and right limits

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:

namespace Chapter9

Definition 9.5.1. We give left and right limits the "junk" value of 0 if the limit does not exist.

abbrev RightLimitExists (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : Prop := ∃ L, (nhdsWithin x₀ (X ∩ .Ioi x₀)).Tendsto f (nhds L)
open Classical in noncomputable abbrev right_limit (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : ℝ := if h : RightLimitExists X f x₀ then h.choose else 0abbrev LeftLimitExists (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : Prop := ∃ L, (nhdsWithin x₀ (X ∩ .Iio x₀)).Tendsto f (nhds L)open Classical in noncomputable abbrev left_limit (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : ℝ := if h: LeftLimitExists X f x₀ then h.choose else 0theorem right_limit.eq {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} {L:ℝ} (had: AdherentPt x₀ (X ∩ .Ioi x₀)) (h: (nhdsWithin x₀ (X ∩ .Ioi x₀)).Tendsto f (nhds L)) : RightLimitExists X f x₀ ∧ right_limit X f x₀ = L := X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)⊢ RightLimitExists X f x₀ ∧ right_limit X f x₀ = L have h' : RightLimitExists X f x₀ := X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)⊢ RightLimitExists X f x₀ ∧ right_limit X f x₀ = L All goals completed! 🐙 X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)h':Chapter9.RightLimitExists _fvar.1432 _fvar.1433 _fvar.1434 := ?_mvar.1444⊢ Exists.choose ⋯ = L have hne : (nhdsWithin x₀ (X ∩ .Ioi x₀)).NeBot := X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)⊢ RightLimitExists X f x₀ ∧ right_limit X f x₀ = L rwa [←mem_closure_iff_nhdsWithin_neBot, closure_def'X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)h':Chapter9.RightLimitExists _fvar.1432 _fvar.1433 _fvar.1434 := ?_mvar.1444⊢ AdherentPt x₀ (X ∩ Set.Ioi x₀) All goals completed! 🐙theorem left_limit.eq {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} {L:ℝ} (had: AdherentPt x₀ (X ∩ .Iio x₀)) (h: (nhdsWithin x₀ (X ∩ .Iio x₀)).Tendsto f (nhds L)) : LeftLimitExists X f x₀ ∧ left_limit X f x₀ = L := X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)⊢ LeftLimitExists X f x₀ ∧ left_limit X f x₀ = L have h' : LeftLimitExists X f x₀ := X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)⊢ LeftLimitExists X f x₀ ∧ left_limit X f x₀ = L All goals completed! 🐙 X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)h':Chapter9.LeftLimitExists _fvar.3517 _fvar.3518 _fvar.3519 := ?_mvar.3529⊢ Exists.choose ⋯ = L have hne : (nhdsWithin x₀ (X ∩ .Iio x₀)).NeBot := X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)⊢ LeftLimitExists X f x₀ ∧ left_limit X f x₀ = L rwa [←mem_closure_iff_nhdsWithin_neBot, closure_def'X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)h':Chapter9.LeftLimitExists _fvar.3517 _fvar.3518 _fvar.3519 := ?_mvar.3529⊢ AdherentPt x₀ (X ∩ Set.Iio x₀) All goals completed! 🐙theorem right_limit.eq' {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (h: RightLimitExists X f x₀) : (nhdsWithin x₀ (X ∩ .Ioi x₀)).Tendsto f (nhds (right_limit X f x₀)) := X:Set ℝf:ℝ → ℝx₀:ℝh:RightLimitExists X f x₀⊢ Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds (right_limit X f x₀)) X:Set ℝf:ℝ → ℝx₀:ℝh:RightLimitExists X f x₀⊢ Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds (Exists.choose ⋯)); All goals completed! 🐙theorem left_limit.eq' {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (h: LeftLimitExists X f x₀) : (nhdsWithin x₀ (X ∩ .Iio x₀)).Tendsto f (nhds (left_limit X f x₀)) := X:Set ℝf:ℝ → ℝx₀:ℝh:LeftLimitExists X f x₀⊢ Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds (left_limit X f x₀)) X:Set ℝf:ℝ → ℝx₀:ℝh:LeftLimitExists X f x₀⊢ Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds (Exists.choose ⋯)); All goals completed! 🐙

Example 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 .univ Real.sign 0 = 1 := ⊢ right_limit Set.univ Real.sign 0 = 1 All goals completed! 🐙
declaration uses 'sorry'example : left_limit .univ Real.sign 0 = -1 := ⊢ left_limit Set.univ Real.sign 0 = -1 All goals completed! 🐙theorem right_limit.conv {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (had: AdherentPt x₀ (X ∩ .Ioi x₀)) (h: RightLimitExists X f x₀) (a:ℕ → ℝ) (ha: ∀ n, a n ∈ X ∩ .Ioi x₀) (hconv: Filter.atTop.Tendsto a (nhds x₀)) : Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds (right_limit X f x₀)) := X:Set ℝf:ℝ → ℝx₀:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:RightLimitExists 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₀)) X:Set ℝf:ℝ → ℝx₀:ℝ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 (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (right_limit X f x₀)) X:Set ℝf:ℝ → ℝx₀:ℝ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 (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)⊢ Convergesto (X ∩ Set.Ioi x₀) f (right_limit X f x₀) x₀ rwa [Convergesto.iff, (eq had hL).2X:Set ℝf:ℝ → ℝx₀:ℝ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 (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)⊢ Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)theorem left_limit.conv {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (had: AdherentPt x₀ (X ∩ .Iio x₀)) (h: LeftLimitExists X f x₀) (a:ℕ → ℝ) (ha: ∀ n, a n ∈ X ∩ .Iio x₀) (hconv: Filter.atTop.Tendsto a (nhds x₀)) : Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds (left_limit X f x₀)) := X:Set ℝf:ℝ → ℝx₀:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:LeftLimitExists 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₀)) X:Set ℝf:ℝ → ℝx₀:ℝ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 (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (left_limit X f x₀)) X:Set ℝf:ℝ → ℝx₀:ℝ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 (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)⊢ Convergesto (X ∩ Set.Iio x₀) f (left_limit X f x₀) x₀ rwa [Convergesto.iff, (eq had hL).2X:Set ℝf:ℝ → ℝx₀:ℝ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 (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)⊢ Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)

Proposition 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 ∩ .Iio x₀)) (had_right: AdherentPt x₀ (X ∩ .Ioi x₀)) : ContinuousWithinAt f X x₀ ↔ (RightLimitExists X f x₀ ∧ right_limit X f x₀ = f x₀) ∧ (LeftLimitExists X f x₀ ∧ left_limit X f x₀ = f x₀) := X: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₀ ↔ (RightLimitExists X f x₀ ∧ right_limit X f x₀ = f x₀) ∧ LeftLimitExists X f x₀ ∧ left_limit X f x₀ = f x₀ -- This proof is written to follow the structure of the original text. X: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₀ → (RightLimitExists X f x₀ ∧ right_limit X f x₀ = f x₀) ∧ LeftLimitExists X f x₀ ∧ left_limit X f x₀ = f x₀X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)⊢ (RightLimitExists X f x₀ ∧ right_limit X f x₀ = f x₀) ∧ LeftLimitExists X f x₀ ∧ left_limit X f x₀ = f x₀ → ContinuousWithinAt f X x₀ X: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₀ → (RightLimitExists X f x₀ ∧ right_limit X f x₀ = f x₀) ∧ LeftLimitExists X f x₀ ∧ left_limit X f x₀ = f x₀ All goals completed! 🐙 X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)hre:RightLimitExists X f x₀hright:right_limit X f x₀ = f x₀hle:LeftLimitExists X f x₀lheft:left_limit X f x₀ = f x₀⊢ ContinuousWithinAt f X x₀ X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)hre:RightLimitExists X f x₀hle:LeftLimitExists X f x₀L:ℝ := @_fvar.10066 _fvar.10067hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = L⊢ ContinuousWithinAt f X x₀ X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)hre:RightLimitExists X f x₀hle:LeftLimitExists X f x₀L:ℝ := @_fvar.10066 _fvar.10067hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:?_mvar.10407 := List.TFAE.out (Chapter9.ContinuousWithinAt.tfae _fvar.10065 _fvar.10066 _fvar.10068) 0 2 ?_mvar.10451 ?_mvar.10452⊢ ContinuousWithinAt f X x₀ X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)hre:RightLimitExists X f x₀hle:LeftLimitExists X f x₀L:ℝ := @_fvar.10066 _fvar.10067hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:?_mvar.10407 := List.TFAE.out (Chapter9.ContinuousWithinAt.tfae _fvar.10065 _fvar.10066 _fvar.10068) 0 2 ?_mvar.10451 ?_mvar.10452⊢ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)hre:RightLimitExists X f x₀hle:LeftLimitExists X f x₀L:ℝ := @_fvar.10066 _fvar.10067hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:?_mvar.10407 := List.TFAE.out (Chapter9.ContinuousWithinAt.tfae _fvar.10065 _fvar.10066 _fvar.10068) 0 2 ?_mvar.10451 ?_mvar.10452ε:ℝhε:ε > 0⊢ ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)hle:LeftLimitExists X f x₀L:ℝ := @_fvar.10066 _fvar.10067hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:?_mvar.10407 := List.TFAE.out (Chapter9.ContinuousWithinAt.tfae _fvar.10065 _fvar.10066 _fvar.10068) 0 2 ?_mvar.10451 ?_mvar.10452ε:ℝhε:ε > 0hre:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds (right_limit X f x₀))⊢ ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := @_fvar.10066 _fvar.10067hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:?_mvar.10407 := List.TFAE.out (Chapter9.ContinuousWithinAt.tfae _fvar.10065 _fvar.10066 _fvar.10068) 0 2 ?_mvar.10451 ?_mvar.10452ε:ℝhε:ε > 0hre:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds (right_limit X f x₀))hle:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds (left_limit X f x₀))⊢ ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := @_fvar.10066 _fvar.10067hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:?_mvar.10407 := List.TFAE.out (Chapter9.ContinuousWithinAt.tfae _fvar.10065 _fvar.10066 _fvar.10068) 0 2 ?_mvar.10451 ?_mvar.10452ε:ℝhε:ε > 0hre:Convergesto (X ∩ Set.Ioi x₀) f L x₀hle:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds (left_limit X f x₀))⊢ ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := @_fvar.10066 _fvar.10067hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:?_mvar.10407 := List.TFAE.out (Chapter9.ContinuousWithinAt.tfae _fvar.10065 _fvar.10066 _fvar.10068) 0 2 ?_mvar.10451 ?_mvar.10452ε:ℝ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₀| < ε X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := @_fvar.10066 _fvar.10067hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:?_mvar.10407 := List.TFAE.out (Chapter9.ContinuousWithinAt.tfae _fvar.10065 _fvar.10066 _fvar.10068) 0 2 ?_mvar.10451 ?_mvar.10452ε:ℝ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₀| < ε X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := @_fvar.10066 _fvar.10067hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:?_mvar.10407 := List.TFAE.out (Chapter9.ContinuousWithinAt.tfae _fvar.10065 _fvar.10066 _fvar.10068) 0 2 ?_mvar.10451 ?_mvar.10452ε:ℝ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| < εδ_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₀| < ε X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := @_fvar.10066 _fvar.10067hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:?_mvar.10407 := List.TFAE.out (Chapter9.ContinuousWithinAt.tfae _fvar.10065 _fvar.10066 _fvar.10068) 0 2 ?_mvar.10451 ?_mvar.10452ε:ℝ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| < εδ_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, (X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := @_fvar.10066 _fvar.10067hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:ContinuousWithinAt _fvar.10066 _fvar.10065 _fvar.10067 ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ _fvar.10065, |x - _fvar.10067| < δ → |@_fvar.10066 x - @_fvar.10066 _fvar.10067| < ε := List.TFAE.out (Chapter9.ContinuousWithinAt.tfae _fvar.10065 _fvar.10066 _fvar.10068) 0 2 (Eq.refl [ContinuousWithinAt _fvar.10066 _fvar.10065 _fvar.10067, ∀ (a : ℕ → ℝ), (∀ (n : ℕ), a n ∈ _fvar.10065) → Filter.Tendsto a Filter.atTop (nhds _fvar.10067) → Filter.Tendsto (fun n => @_fvar.10066 (a n)) Filter.atTop (nhds (@_fvar.10066 _fvar.10067)), ∀ ε > 0, ∃ δ > 0, ∀ x ∈ _fvar.10065, |x - _fvar.10067| < δ → |@_fvar.10066 x - @_fvar.10066 _fvar.10067| < ε][0]?) (Eq.refl [ContinuousWithinAt _fvar.10066 _fvar.10065 _fvar.10067, ∀ (a : ℕ → ℝ), (∀ (n : ℕ), a n ∈ _fvar.10065) → Filter.Tendsto a Filter.atTop (nhds _fvar.10067) → Filter.Tendsto (fun n => @_fvar.10066 (a n)) Filter.atTop (nhds (@_fvar.10066 _fvar.10067)), ∀ ε > 0, ∃ δ > 0, ∀ x ∈ _fvar.10065, |x - _fvar.10067| < δ → |@_fvar.10066 x - @_fvar.10066 _fvar.10067| < ε][2]?)ε:ℝ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| < εδ_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 All goals completed! 🐙) X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := @_fvar.10066 _fvar.10067hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:?_mvar.10407 := List.TFAE.out (Chapter9.ContinuousWithinAt.tfae _fvar.10065 _fvar.10066 _fvar.10068) 0 2 ?_mvar.10451 ?_mvar.10452ε:ℝ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| < εδ_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₀| < ε X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := @_fvar.10066 _fvar.10067hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:?_mvar.10407 := List.TFAE.out (Chapter9.ContinuousWithinAt.tfae _fvar.10065 _fvar.10066 _fvar.10068) 0 2 ?_mvar.10451 ?_mvar.10452ε:ℝ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| < εδ_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₀| < εX:Set ℝf:ℝ → ℝε:ℝhε:ε > 0δ_plus:ℝhδ_plus:0 < δ_plusδ_minus:ℝhδ_minus:0 < δ_minusx:ℝhx:x ∈ Xh:x ∈ Xhad_left:AdherentPt x (X ∩ Set.Iio x)had_right:AdherentPt x (X ∩ Set.Ioi x)L:ℝ := @_fvar.10066 _fvar.74473hright:right_limit X f x = Llheft:left_limit X f x = Lthis:ContinuousWithinAt f X x ↔ ∀ ε > 0, ∃ δ > 0, ∀ x_1 ∈ X, |x_1 - x| < δ → |f x_1 - f x| < εhre✝:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ x_1 ∈ X, x < x_1 → x - δ < x_1 → x_1 < x + δ → |f x_1 - L| < εhle✝:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ x_1 ∈ X, x_1 < x → x - δ < x_1 → x_1 < x + δ → |f x_1 - L| < εhre:∀ x_1 ∈ X, x < x_1 → x - δ_plus < x_1 → x_1 < x + δ_plus → |f x_1 - L| < εhle:∀ x_1 ∈ X, x_1 < x → x - δ_minus < x_1 → x_1 < x + δ_minus → |f x_1 - L| < εhxx₀:|x - x| < min δ_plus δ_minus⊢ |f x - f x| < εX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := @_fvar.10066 _fvar.10067hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:?_mvar.10407 := List.TFAE.out (Chapter9.ContinuousWithinAt.tfae _fvar.10065 _fvar.10066 _fvar.10068) 0 2 ?_mvar.10451 ?_mvar.10452ε:ℝ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| < εδ_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₀| < ε X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xhad_left:AdherentPt x₀ (X ∩ Set.Iio x₀)had_right:AdherentPt x₀ (X ∩ Set.Ioi x₀)L:ℝ := @_fvar.10066 _fvar.10067hright:right_limit X f x₀ = Llheft:left_limit X f x₀ = Lthis:?_mvar.10407 := List.TFAE.out (Chapter9.ContinuousWithinAt.tfae _fvar.10065 _fvar.10066 _fvar.10068) 0 2 ?_mvar.10451 ?_mvar.10452ε:ℝ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| < εδ_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₀| < ε All goals completed! 🐙 X:Set ℝf:ℝ → ℝε:ℝhε:ε > 0δ_plus:ℝhδ_plus:0 < δ_plusδ_minus:ℝhδ_minus:0 < δ_minusx:ℝhx:x ∈ Xh:x ∈ Xhad_left:AdherentPt x (X ∩ Set.Iio x)had_right:AdherentPt x (X ∩ Set.Ioi x)L:ℝ := @_fvar.10066 _fvar.74473hright:right_limit X f x = Llheft:left_limit X f x = Lthis:ContinuousWithinAt f X x ↔ ∀ ε > 0, ∃ δ > 0, ∀ x_1 ∈ X, |x_1 - x| < δ → |f x_1 - f x| < εhre✝:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ x_1 ∈ X, x < x_1 → x - δ < x_1 → x_1 < x + δ → |f x_1 - L| < εhle✝:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ x_1 ∈ X, x_1 < x → x - δ < x_1 → x_1 < x + δ → |f x_1 - L| < εhre:∀ x_1 ∈ X, x < x_1 → x - δ_plus < x_1 → x_1 < x + δ_plus → |f x_1 - L| < εhle:∀ x_1 ∈ X, x_1 < x → x - δ_minus < x_1 → x_1 < x + δ_minus → |f x_1 - L| < εhxx₀:|x - x| < min δ_plus δ_minus⊢ |f x - f x| < ε All goals completed! 🐙 All goals completed! 🐙
abbrev HasJumpDiscontinuity (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : Prop := RightLimitExists X f x₀ ∧ LeftLimitExists X f x₀ ∧ right_limit X f x₀ ≠ left_limit X f x₀declaration uses 'sorry'example : HasJumpDiscontinuity .univ Real.sign 0 := ⊢ HasJumpDiscontinuity Set.univ Real.sign 0 All goals completed! 🐙abbrev HasRemovableDiscontinuity (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : Prop := RightLimitExists X f x₀ ∧ LeftLimitExists X f x₀ ∧ right_limit X f x₀ = left_limit X f x₀ ∧ right_limit X f x₀ ≠ f x₀declaration uses 'sorry'example : HasRemovableDiscontinuity .univ f_9_3_17 0 := ⊢ HasRemovableDiscontinuity Set.univ f_9_3_17 0 All goals completed! 🐙declaration uses 'sorry'example : ¬ HasRemovableDiscontinuity .univ (fun x ↦ 1/x) 0 := ⊢ ¬HasRemovableDiscontinuity Set.univ (fun x => 1 / x) 0 All goals completed! 🐙declaration uses 'sorry'example : ¬ HasJumpDiscontinuity .univ (fun x ↦ 1/x) 0 := ⊢ ¬HasJumpDiscontinuity Set.univ (fun x => 1 / x) 0 All goals completed! 🐙/- Exercise 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