def IsClusterPoint (S : Set ℝ) (x : ℝ) : Prop

Definition 3.1.1: For a set S ⊆ ℝ, a real number x is a cluster point of S if for every ε > 0 the punctured neighborhood (x - ε, x + ε) ∩ S \ {x} is nonempty.

Equations

• IsClusterPoint S x = ∀ ⦃ε : ℝ⦄, 0 < ε → ((Set.Ioo (x - ε) (x + ε) ∩ S) \ {x}).Nonempty

theorem isClusterPoint_iff_mem_closure_diff (S : Set ℝ) (x : ℝ) : IsClusterPoint S x ↔ x ∈ closure (S \ {x})

Mathlib expresses cluster points via closure of punctured sets.

theorem isClusterPoint_iff_exists_seq_tendsto (S : Set ℝ) (x : ℝ) : IsClusterPoint S x ↔ ∃ (u : ℕ → ℝ), (∀ (n : ℕ), u n ∈ S ∧ u n ≠ x) ∧ Filter.Tendsto u Filter.atTop (nhds x)

Proposition 3.1.2: A real number x is a cluster point of S ⊆ ℝ iff there exists a sequence (xₙ) with each xₙ ∈ S, xₙ ≠ x, and xₙ → x.

def LimitWithin (S : Set ℝ) (f : ℝ → ℝ) (c L : ℝ) : Prop

Definition 3.1.3: A function f : ℝ → ℝ converges to L as x approaches c within a set S if c is a cluster point of S and for every ε > 0 there is δ > 0 such that for all x ∈ S with x ≠ c and |x - c| < δ we have |f x - L| < ε.

Equations

• LimitWithin S f c L = (IsClusterPoint S c ∧ ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ S → x ≠ c → |x - c| < δ → |f x - L| < ε)

theorem exists_mem_near_cluster {S : Set ℝ} {c δ : ℝ} (hc : IsClusterPoint S c) (hδ : 0 < δ) : ∃ x ∈ S, x ≠ c ∧ |x - c| < δ

Given a cluster point and a radius, we can find a point of the set that lies within that radius yet differs from the center.

theorem abs_sub_lt_of_add {a b c ε : ℝ} (h₁ : |a - b| < ε / 2) (h₂ : |b - c| < ε / 2) : |a - c| < ε

A quantitative triangle inequality specialized to halving an epsilon.

theorem mem_diff_singleton_iff {S : Set ℝ} {x c : ℝ} : x ∈ S \ {c} ↔ x ∈ S ∧ x ≠ c

Membership in S \ {c} means membership in S and inequality to c.

theorem limitWithin_to_tendsto {S : Set ℝ} {f : ℝ → ℝ} {c L : ℝ} : LimitWithin S f c L → Filter.Tendsto f (nhdsWithin c (S \ {c})) (nhds L)

Convert LimitWithin to a Tendsto statement on S \ {c}.

theorem tendsto_to_limitWithin_epsdelta {S : Set ℝ} {f : ℝ → ℝ} {c L : ℝ} : Filter.Tendsto f (nhdsWithin c (S \ {c})) (nhds L) → ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ S → x ≠ c → |x - c| < δ → |f x - L| < ε

Repackage a Tendsto statement on S \ {c} into eps-delta form.

theorem limitWithin_iff_tendsto (S : Set ℝ) (f : ℝ → ℝ) (c L : ℝ) : LimitWithin S f c L ↔ IsClusterPoint S c ∧ Filter.Tendsto f (nhdsWithin c (S \ {c})) (nhds L)

Mathlib expresses this limit as a Tendsto statement toward the nhdsWithin filter that omits the point c.

theorem limitWithin_unique (S : Set ℝ) (f : ℝ → ℝ) (c L₁ L₂ : ℝ) (h₁ : LimitWithin S f c L₁) (h₂ : LimitWithin S f c L₂) : L₁ = L₂

Proposition 3.1.4: If c is a cluster point of S ⊆ ℝ and a function f : ℝ → ℝ converges to some real number as x approaches c within S, then that limit value is unique.

theorem abs_le_of_abs_sub_lt_one {x c : ℝ} (h : |x - c| < 1) : |x| ≤ |c| + 1

Bounding |x| when x lies within 1 of c.

theorem abs_sq_sub_bound {x c : ℝ} (h : |x - c| < 1) : |x ^ 2 - c ^ 2| ≤ (2 * |c| + 1) * |x - c|

Bounding |x^2 - c^2| by |x - c| when x is within 1 of c.

theorem tendsto_sq (c : ℝ) : Filter.Tendsto (fun (x : ℝ) => x ^ 2) (nhds c) (nhds (c ^ 2))

Example 3.1.5: For the function f x = x^2 and any real c, the limit as x → c is c^2.

noncomputable def limitValueDiff (x : ℝ) : ℝ

Example 3.1.6: The piecewise function on [0, 1) given by f x = x for x > 0 and f 0 = 1 satisfies f ⟶ 0 as x → 0 within [0, 1), even though f 0 = 1.

Equations

• limitValueDiff x = if x = 0 then 1 else x

theorem limitValueDiff_of_ne_zero {x : ℝ} (hx : x ≠ 0) : limitValueDiff x = x

theorem limitValueDiff_eq_self_of_mem_Ioo {x : ℝ} (hx : x ∈ Set.Ioo 0 1) : limitValueDiff x = x

theorem abs_limitValueDiff_eq_of_mem_Ioo {x : ℝ} (hx : x ∈ Set.Ioo 0 1) : |limitValueDiff x| = x

theorem tendsto_limitValueDiff : Filter.Tendsto limitValueDiff (nhdsWithin 0 (Set.Ioo 0 1)) (nhds 0)

The limit of limitValueDiff at 0 within (0, 1) (the punctured part of [0, 1)) is 0.

theorem limitValueDiff_zero : limitValueDiff 0 = 1

The value of limitValueDiff at 0 is 1, differing from the limit.

theorem limitWithin_iff_seq_tendsto (S : Set ℝ) (f : ℝ → ℝ) (c L : ℝ) : LimitWithin S f c L ↔ IsClusterPoint S c ∧ ∀ (u : ℕ → ℝ), (∀ (n : ℕ), u n ∈ S \ {c}) → Filter.Tendsto u Filter.atTop (nhds c) → Filter.Tendsto (fun (n : ℕ) => f (u n)) Filter.atTop (nhds L)

Lemma 3.1.7: For S ⊆ ℝ, a cluster point c of S, a function f : S → ℝ, and L : ℝ, we have f(x) → L as x → c iff for every sequence (xₙ) with xₙ ∈ S \ {c} and xₙ → c, the sequence (f xₙ) converges to L.

noncomputable def sinInvSeq (n : ℕ) : ℝ

The sequence uₙ = 1 / (π n + π / 2) used in Example 3.1.8.

Equations

• sinInvSeq n = 1 / (Real.pi * ↑n + Real.pi / 2)

theorem sinInvSeq_den_pos (n : ℕ) : 0 < Real.pi * ↑n + Real.pi / 2

theorem sinInvSeq_pos (n : ℕ) : 0 < sinInvSeq n

theorem sinInvSeq_ne_zero (n : ℕ) : sinInvSeq n ≠ 0

theorem sinInvSeq_eq (n : ℕ) : sinInvSeq n = 1 / Real.pi * (1 / (↑n + 1 / 2))

theorem sin_inv_seq_tendsto : Filter.Tendsto sinInvSeq Filter.atTop (nhds 0)

theorem sin_inv_seq_values (n : ℕ) : Real.sin (1 / sinInvSeq n) = (-1) ^ n

theorem sin_inv_seq_values' (n : ℕ) : Real.sin (sinInvSeq n)⁻¹ = (-1) ^ n

theorem pow_neg_one_not_convergent : ¬∃ (L : ℝ), Filter.Tendsto (fun (n : ℕ) => (-1) ^ n) Filter.atTop (nhds L)

theorem seq_mul_sin_inv_tendsto_zero {v : ℕ → ℝ} (hv_zero : Filter.Tendsto v Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => v n * Real.sin (1 / v n)) Filter.atTop (nhds 0)

theorem sin_inv_no_limit : ¬∃ (L : ℝ), LimitWithin Set.univ (fun (x : ℝ) => Real.sin (1 / x)) 0 L

Example 3.1.8: The limit of sin (1 / x) as x → 0 does not exist, but the limit of x * sin (1 / x) as x → 0 equals 0.

theorem limit_mul_sin_inv : LimitWithin Set.univ (fun (x : ℝ) => x * Real.sin (1 / x)) 0 0

The product x * sin (1 / x) converges to 0 as x → 0.

theorem seq_limit_le {a b : ℕ → ℝ} {L₁ L₂ : ℝ} (ha : Filter.Tendsto a Filter.atTop (nhds L₁)) (hb : Filter.Tendsto b Filter.atTop (nhds L₂)) (hmono : ∀ (n : ℕ), a n ≤ b n) : L₁ ≤ L₂

If two real sequences converge and one bounds the other termwise, then their limits respect the same inequality.

theorem limitWithin_le_of_le {S : Set ℝ} {c Lf Lg : ℝ} {f g : ℝ → ℝ} (hf : LimitWithin S f c Lf) (hg : LimitWithin S g c Lg) (hfg : ∀ ⦃x : ℝ⦄, x ∈ S → x ≠ c → f x ≤ g x) : Lf ≤ Lg

Corollary 3.1.9: If c is a cluster point of S ⊆ ℝ, f, g : ℝ → ℝ have limits L_f, L_g as x → c within S, and f x ≤ g x for all x ∈ S \ {c}, then L_f ≤ L_g.

theorem limitWithin_mem_interval {S : Set ℝ} {c L a b : ℝ} {f : ℝ → ℝ} (hlim : LimitWithin S f c L) (hbounds : ∀ ⦃x : ℝ⦄, x ∈ S \ {c} → a ≤ f x ∧ f x ≤ b) : a ≤ L ∧ L ≤ b

Corollary 3.1.10: If c is a cluster point of S ⊆ ℝ, f : ℝ → ℝ has a limit L as x → c within S, and a ≤ f x ≤ b for all x ∈ S \ {c}, then a ≤ L ≤ b.

theorem limitWithin_squeeze {S : Set ℝ} {c L : ℝ} {f g h : ℝ → ℝ} (hf : LimitWithin S f c L) (hh : LimitWithin S h c L) (hfg : ∀ ⦃x : ℝ⦄, x ∈ S → x ≠ c → f x ≤ g x) (hgh : ∀ ⦃x : ℝ⦄, x ∈ S → x ≠ c → g x ≤ h x) : LimitWithin S g c L

Corollary 3.1.11 (squeeze theorem): Let S ⊆ ℝ and c be a cluster point of S. If f, g, h : ℝ → ℝ satisfy f x ≤ g x ≤ h x for all x ∈ S \ {c} and f and h both have limit L as x → c within S, then g also has limit L as x → c within S.

theorem limitWithin_add {S : Set ℝ} {c Lf Lg : ℝ} {f g : ℝ → ℝ} (hf : LimitWithin S f c Lf) (hg : LimitWithin S g c Lg) : LimitWithin S (fun (x : ℝ) => f x + g x) c (Lf + Lg)

Corollary 3.1.12: Let S ⊆ ℝ and c be a cluster point of S. If f, g : ℝ → ℝ have limits as x → c within S, then (i) the limit of f + g equals the sum of the limits, (ii) the limit of f - g equals the difference of the limits, (iii) the limit of f * g equals the product of the limits, and (iv) if the limit of g is nonzero and g x ≠ 0 for all x ∈ S \ {c}, then the limit of f / g equals the quotient of the limits.

theorem limitWithin_sub {S : Set ℝ} {c Lf Lg : ℝ} {f g : ℝ → ℝ} (hf : LimitWithin S f c Lf) (hg : LimitWithin S g c Lg) : LimitWithin S (fun (x : ℝ) => f x - g x) c (Lf - Lg)

theorem limitWithin_mul {S : Set ℝ} {c Lf Lg : ℝ} {f g : ℝ → ℝ} (hf : LimitWithin S f c Lf) (hg : LimitWithin S g c Lg) : LimitWithin S (fun (x : ℝ) => f x * g x) c (Lf * Lg)

theorem limitWithin_div {S : Set ℝ} {c Lf Lg : ℝ} {f g : ℝ → ℝ} (hf : LimitWithin S f c Lf) (hg : LimitWithin S g c Lg) (hg0 : ∀ ⦃x : ℝ⦄, x ∈ S → x ≠ c → g x ≠ 0) (hL0 : Lg ≠ 0) : LimitWithin S (fun (x : ℝ) => f x / g x) c (Lf / Lg)

theorem limitWithin_abs {S : Set ℝ} {c L : ℝ} {f : ℝ → ℝ} (hlim : LimitWithin S f c L) : LimitWithin S (fun (x : ℝ) => |f x|) c |L|

Corollary 3.1.13: If S ⊆ ℝ, c is a cluster point of S, and the limit lim_{x → c, x ∈ S} f x exists for a function f : ℝ → ℝ, then the limit of |f x| as x → c within S equals the absolute value of the limit of f.

def restrictToSubset {S A : Set ℝ} (f : ↑S → ℝ) (hAS : A ⊆ S) : ↑A → ℝ

Definition 3.1.14: For a function f : S → ℝ and a subset A ⊆ S, the restriction f|_A : A → ℝ is given by f|_A x = f x for x ∈ A.

Equations

• restrictToSubset f hAS x = f ⟨↑x, ⋯⟩

theorem clusterPoint_iff_of_local_agree {S A : Set ℝ} {c α : ℝ} (hα : 0 < α) (hA : A \ {c} ∩ Set.Ioo (c - α) (c + α) = S \ {c} ∩ Set.Ioo (c - α) (c + α)) : IsClusterPoint A c ↔ IsClusterPoint S c

Proposition 3.1.15(i): If A ⊆ S ⊆ ℝ agree with S on a punctured neighborhood of c (i.e., there exists α > 0 with (A \ {c}) ∩ (c-α, c+α) = (S \ {c}) ∩ (c-α, c+α)), then c is a cluster point of A iff it is a cluster point of S.

theorem limitWithin_imp_of_local_agree {S A : Set ℝ} {c α L : ℝ} {f : ℝ → ℝ} (hα : 0 < α) (hA : A \ {c} ∩ Set.Ioo (c - α) (c + α) = S \ {c} ∩ Set.Ioo (c - α) (c + α)) (hlim : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ S → x ≠ c → |x - c| < δ → |f x - L| < ε) ⦃ε : ℝ⦄ : 0 < ε → ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ A → x ≠ c → |x - c| < δ → |f x - L| < ε

The ε–δ condition for the limit within S implies the corresponding condition within A provided the sets coincide on a punctured neighborhood of c.

theorem limitWithin_iff_of_local_agree {S A : Set ℝ} {c α L : ℝ} {f : ℝ → ℝ} (hα : 0 < α) (hA : A \ {c} ∩ Set.Ioo (c - α) (c + α) = S \ {c} ∩ Set.Ioo (c - α) (c + α)) : IsClusterPoint S c → (LimitWithin S f c L ↔ LimitWithin A f c L)

Proposition 3.1.15(ii): Under the same local agreement near c and assuming c is a cluster point of S, the limit of f along S at c equals that of its restriction to A.

def RightLimitWithin (S : Set ℝ) (f : ℝ → ℝ) (c L : ℝ) : Prop

Definition 3.1.16: For a function f : ℝ → ℝ, the right-hand limit of f at c along a set S is the limit of the restriction of f to S ∩ (c, ∞) as x → c. The left-hand limit is defined analogously using S ∩ (-∞, c).

Equations

• RightLimitWithin S f c L = LimitWithin (S ∩ Set.Ioi c) f c L

def LeftLimitWithin (S : Set ℝ) (f : ℝ → ℝ) (c L : ℝ) : Prop

The left-hand limit of f at c along S, given by restricting to S ∩ (-∞, c) and taking the limit as x → c.

Equations

• LeftLimitWithin S f c L = LimitWithin (S ∩ Set.Iio c) f c L

theorem rightLimitWithin_iff_tendsto (S : Set ℝ) (f : ℝ → ℝ) (c L : ℝ) : RightLimitWithin S f c L ↔ IsClusterPoint (S ∩ Set.Ioi c) c ∧ Filter.Tendsto f (nhdsWithin c (S ∩ Set.Ioi c)) (nhds L)

Right-hand limits coincide with mathlib's Tendsto along the 𝓝 within the right half-neighborhood.

theorem leftLimitWithin_iff_tendsto (S : Set ℝ) (f : ℝ → ℝ) (c L : ℝ) : LeftLimitWithin S f c L ↔ IsClusterPoint (S ∩ Set.Iio c) c ∧ Filter.Tendsto f (nhdsWithin c (S ∩ Set.Iio c)) (nhds L)

Left-hand limits coincide with mathlib's Tendsto along the 𝓝 within the left half-neighborhood.

theorem limitWithin_iff_left_right {S : Set ℝ} {c L : ℝ} {f : ℝ → ℝ} (hleft : IsClusterPoint (S ∩ Set.Iio c) c) (hright : IsClusterPoint (S ∩ Set.Ioi c) c) : IsClusterPoint S c ∧ (LimitWithin S f c L ↔ LeftLimitWithin S f c L ∧ RightLimitWithin S f c L)

Proposition 3.1.17: If c is a cluster point of both S ∩ (-∞, c) and S ∩ (c, ∞), then c is a cluster point of S, and f(x) → L as x → c within S iff both the left-hand and right-hand limits along S equal L.