def IsLimitAlong {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (E : Set X) (f : ↑E → Y) (x0 : X) (L : Y) : Prop

Definition 3.1: [Limiting value of a function] The limit of f at x0 along E is L if x0 is an adherent point of E and for every ε > 0 there exists δ > 0 such that for all x ∈ E, dist x x0 < δ implies dist (f x) L < ε.

Equations

• IsLimitAlong E f x0 L = (x0 ∈ closure E ∧ ∀ ε > 0, ∃ δ > 0, ∀ (x : ↑E), dist (↑x) x0 < δ → dist (f x) L < ε)

theorem helperForProp_3_1_unpuncturedEpsDelta_iff_punctured {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X → Y) (x0 : X) : (∀ ε > 0, ∃ δ > 0, ∀ (x : X), dist x x0 < δ → dist (f x) (f x0) < ε) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x : X), 0 < dist x x0 ∧ dist x x0 < δ → dist (f x) (f x0) < ε

Helper for Proposition 3.1: equivalence between unpunctured and punctured epsilon-delta conditions.

theorem helperForProp_3_1_continuousAt_iff_punctured {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X → Y) (x0 : X) : ContinuousAt f x0 ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x : X), 0 < dist x x0 ∧ dist x x0 < δ → dist (f x) (f x0) < ε

Helper for Proposition 3.1: punctured epsilon-delta characterization of continuity at a point.

theorem continuousAt_iff_limit_and_continuous_iff_limit_all {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X → Y) (x0 : X) : (ContinuousAt f x0 ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x : X), 0 < dist x x0 ∧ dist x x0 < δ → dist (f x) (f x0) < ε) ∧ (Continuous f ↔ ∀ (x1 : X), ∀ ε > 0, ∃ δ > 0, ∀ (x : X), 0 < dist x x1 ∧ dist x x1 < δ → dist (f x) (f x1) < ε)

Proposition 3.1: A function between metric spaces is continuous at x0 iff for every ε > 0 there exists δ > 0 such that 0 < dist x x0 < δ implies dist (f x) (f x0) < ε; consequently, f is continuous on X iff this holds for all x0.

theorem helperForExample_3_1_1_continuousAt_quadraticMinusFour : ContinuousAt (fun (x : ℝ) => x ^ 2 - 4) 1

Helper for Example 3.1.1: continuity of x ↦ x^2 - 4 at 1.

theorem limit_quadratic_minus_four_at_one : IsLimitAlong Set.univ (fun (x : ↑Set.univ) => ↑x ^ 2 - 4) 1 (1 ^ 2 - 4) ∧ 1 ^ 2 - 4 = -3

Example 3.1.1: If f : Real → Real is the function f x = x^2 - 4, then lim_{x → 1} f(x) = f(1) = 1 - 4 = -3 since f is continuous.

def IsLimitAlongPunctured {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (E : Set X) (f : ↑E → Y) (x0 : X) (L : Y) : Prop

The punctured epsilon-delta limit along E at x0, excluding the base point.

Equations

• IsLimitAlongPunctured E f x0 L = ∀ ε > 0, ∃ δ > 0, ∀ (x : ↑E), 0 < dist (↑x) x0 ∧ dist (↑x) x0 < δ → dist (f x) L < ε

theorem helperForProposition_3_2_mem_of_mem_union_singleton_ne {X : Type u_1} (E : Set X) (x0 x : X) (hx : x ∈ E ∪ {x0}) (hx0 : x ≠ x0) : x ∈ E

Helper for Proposition 3.2: points in E ∪ {x0} distinct from x0 lie in E.

theorem helperForProposition_3_2_isLimitPunctured_of_subset_singleton {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (E : Set X) (f : ↑E → Y) (x0 : X) (L : Y) (hE : E ⊆ {x0}) : IsLimitAlongPunctured E f x0 L

Helper for Proposition 3.2: if E ⊆ {x0}, the punctured limit holds for any L.

theorem helperForProposition_3_2_seqCondition_of_subset_singleton {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (E : Set X) (f : ↑E → Y) (x0 : X) (L : Y) (hE : E ⊆ {x0}) (x : ℕ → ↑E) : Filter.Tendsto (fun (n : ℕ) => ↑(x n)) Filter.atTop (nhds x0) → (∀ (n : ℕ), ↑(x n) ≠ x0) → Filter.Tendsto (fun (n : ℕ) => f (x n)) Filter.atTop (nhds L)

Helper for Proposition 3.2: if E ⊆ {x0}, the sequential condition is vacuous.

theorem helperForProposition_3_2_openCondition_of_subset_singleton {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (E : Set X) (f : ↑E → Y) (x0 : X) (L : Y) (hE : E ⊆ {x0}) (V : Set Y) : IsOpen V → L ∈ V → ∃ (U : Set X), IsOpen U ∧ x0 ∈ U ∧ ∀ (x : ↑E), ↑x ∈ U → ↑x ≠ x0 → f x ∈ V

Helper for Proposition 3.2: if E ⊆ {x0}, the open-set condition is vacuous.

noncomputable def limitExtension {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (E : Set X) (f : ↑E → Y) (x0 : X) (L : Y) : { x : X // x ∈ E ∪ {x0} } → Y

The extension of f to E ∪ {x0} taking the value L at x0.

Equations

• limitExtension E f x0 L x = if hx0 : ↑x = x0 then L else f ⟨↑x, ⋯⟩

theorem helperForProposition_3_2_eq_x0_of_mem_union_singleton {X : Type u_1} (E : Set X) (x0 : X) (hE : E ⊆ {x0}) (x : { x : X // x ∈ E ∪ {x0} }) : ↑x = x0

Helper for Proposition 3.2: points of E ∪ {x0} are equal to x0 when E ⊆ {x0}.

theorem helperForProposition_3_2_limitExtension_eq_L_of_eq {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (E : Set X) (f : ↑E → Y) (x0 : X) (L : Y) (x : { x : X // x ∈ E ∪ {x0} }) (hx : ↑x = x0) : limitExtension E f x0 L x = L

Helper for Proposition 3.2: the limit extension takes value L when x = x0.

theorem mem_union_singleton_self {X : Type u_1} (E : Set X) (x0 : X) : x0 ∈ E ∪ {x0}

The base point x0 lies in E ∪ {x0}.

theorem helperForProposition_3_2_continuousAt_limitExtension_of_subset_singleton {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (E : Set X) (f : ↑E → Y) (x0 : X) (L : Y) (hE : E ⊆ {x0}) : ContinuousAt (limitExtension E f x0 L) ⟨x0, ⋯⟩

Helper for Proposition 3.2: continuity of the limit extension for E ⊆ {x0}.

theorem helperForProposition_3_2_punctured_iff_sequence {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (E : Set X) (f : ↑E → Y) (x0 : X) (L : Y) : IsLimitAlongPunctured E f x0 L ↔ ∀ (x : ℕ → ↑E), Filter.Tendsto (fun (n : ℕ) => ↑(x n)) Filter.atTop (nhds x0) → (∀ (n : ℕ), ↑(x n) ≠ x0) → Filter.Tendsto (fun (n : ℕ) => f (x n)) Filter.atTop (nhds L)

Helper for Proposition 3.2: punctured epsilon-delta limit iff sequential criterion.

theorem helperForProposition_3_2_punctured_iff_open {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (E : Set X) (f : ↑E → Y) (x0 : X) (L : Y) : IsLimitAlongPunctured E f x0 L ↔ ∀ (V : Set Y), IsOpen V → L ∈ V → ∃ (U : Set X), IsOpen U ∧ x0 ∈ U ∧ ∀ (x : ↑E), ↑x ∈ U → ↑x ≠ x0 → f x ∈ V

Helper for Proposition 3.2: punctured epsilon-delta limit iff open-set criterion.

theorem helperForProposition_3_2_counterexample_isolated_point : ∃ (E : Set ℝ) (f : ↑E → ℝ) (x0 : ℝ) (L : ℝ), x0 ∈ closure E ∧ IsLimitAlongPunctured E f x0 L ∧ (∀ (x : ℕ → ↑E), Filter.Tendsto (fun (n : ℕ) => ↑(x n)) Filter.atTop (nhds x0) → (∀ (n : ℕ), ↑(x n) ≠ x0) → Filter.Tendsto (fun (n : ℕ) => f (x n)) Filter.atTop (nhds L)) ∧ (∀ (V : Set ℝ), IsOpen V → L ∈ V → ∃ (U : Set ℝ), IsOpen U ∧ x0 ∈ U ∧ ∀ (x : ↑E), ↑x ∈ U → ↑x ≠ x0 → f x ∈ V) ∧ ContinuousAt (limitExtension E f x0 L) ⟨x0, ⋯⟩ ∧ ∃ (hx0E : x0 ∈ E), ContinuousAt f ⟨x0, hx0E⟩ ∧ f ⟨x0, hx0E⟩ ≠ L

Helper for Proposition 3.2: isolated-point counterexample to the extra clause.

theorem helperForProposition_3_2_value_eq_of_nonisolated_and_puncturedLimit_and_continuousAt {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (E : Set X) (f : ↑E → Y) (x0 : X) (L : Y) (hx0cl : x0 ∈ closure (E \ {x0})) : IsLimitAlongPunctured E f x0 L → ∀ (hx0E : x0 ∈ E), ContinuousAt f ⟨x0, hx0E⟩ → f ⟨x0, hx0E⟩ = L

Helper for Proposition 3.2: a non-isolated base point forces f x0 = L from a punctured limit and continuity on E.

theorem limit_along_equiv_sequence_open_continuous {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (E : Set X) (f : ↑E → Y) (x0 : X) (L : Y) : x0 ∈ closure E → (IsLimitAlongPunctured E f x0 L ↔ ∀ (x : ℕ → ↑E), Filter.Tendsto (fun (n : ℕ) => ↑(x n)) Filter.atTop (nhds x0) → (∀ (n : ℕ), ↑(x n) ≠ x0) → Filter.Tendsto (fun (n : ℕ) => f (x n)) Filter.atTop (nhds L)) ∧ ((∀ (x : ℕ → ↑E), Filter.Tendsto (fun (n : ℕ) => ↑(x n)) Filter.atTop (nhds x0) → (∀ (n : ℕ), ↑(x n) ≠ x0) → Filter.Tendsto (fun (n : ℕ) => f (x n)) Filter.atTop (nhds L)) ↔ ∀ (V : Set Y), IsOpen V → L ∈ V → ∃ (U : Set X), IsOpen U ∧ x0 ∈ U ∧ ∀ (x : ↑E), ↑x ∈ U → ↑x ≠ x0 → f x ∈ V) ∧ ((∀ (V : Set Y), IsOpen V → L ∈ V → ∃ (U : Set X), IsOpen U ∧ x0 ∈ U ∧ ∀ (x : ↑E), ↑x ∈ U → ↑x ≠ x0 → f x ∈ V) ↔ ContinuousAt (limitExtension E f x0 L) ⟨x0, ⋯⟩ ∧ (x0 ∈ closure (E \ {x0}) → ∀ (hx0E : x0 ∈ E), ContinuousAt f ⟨x0, hx0E⟩ → f ⟨x0, hx0E⟩ = L))

Proposition 3.2: Let E ⊆ X and f : E → Y, and let x0 be an adherent point of E with L ∈ Y. The following are equivalent: (a) the punctured epsilon-delta limit of f along E at x0 equals L; (b) for every sequence in E converging to x0 with all terms distinct from x0, the sequence of f-values converges to L; (c) for every open V ⊆ Y with L ∈ V, there is an open U ⊆ X with x0 ∈ U such that f(U ∩ E \ {x0}) ⊆ V; (d) the extension g to E ∪ {x0} with g(x0)=L and g|_{E\{x0}} = f is continuous at x0, and if x0 ∈ E and f is continuous at x0 (as a function on E), then f x0 = L.

theorem limit_along_unique {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (E : Set X) (f : ↑E → Y) (x0 : X) (L M : Y) (hL : IsLimitAlong E f x0 L) (hM : IsLimitAlong E f x0 M) : L = M

Proposition 3.3: [Uniqueness of limit] If the limit of f at x0 along E equals both L and M, then L = M.