How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The -neighbourhood and the punctured -neighbourhood of a point of
Definition
Throughout, is the complete ordered field (Complete ordered field (least-upper-bound property), Ordered field) with its order (Order on the reals) and its absolute value (Absolute value in an ordered field).
Let and let with . The -neighbourhood of is
and the punctured -neighbourhood of is
The two descriptions of agree because holds exactly when (Basic properties of the absolute value).
A neighbourhood is an open interval. For every and every ,
the interval of Intervals of : the nine order-convex forms, nondegeneracy, and length. Indeed Basic properties of the absolute value gives, for , the equivalence , and adding throughout turns the right-hand side into (Ordered field).
The centre lies in its own neighbourhoods. , since (Basic properties of the absolute value).
Punctured neighbourhoods are never empty. The element satisfies , which is and , so (Basic properties of the absolute value, Ordered field).
Monotonicity in the radius. If then , because (Ordered field).
Nesting at an interior point. If and , then
Indeed for the triangle inequality (The triangle inequality) gives . Note that precisely because , so such a always exists.
Remarks
-
The radius is a real number, not a rational. Nothing on this page tests a condition against rational radii only. That convention belongs to Limits and Cauchy sequences of reals, where the quantifier is over rational and the passage between the rational and the real form is the sanctioned remark of Sequences of reals: bounded, eventually, frequently, tails, subsequences. Here ranges over the positive reals throughout, and every statement above is proved for an arbitrary positive real.
-
Why the punctured version is separated out. A limit point of a set is a point every punctured neighbourhood of which meets the set (Limit point, isolated point, adherent point, derived set, and dense subset of ), and deleting the centre is exactly what stops a point of the set from qualifying automatically. The unpunctured condition defines the weaker notion of an adherent point, and the difference between the two is precisely an isolated point.
-
Nesting is the workhorse. Almost every openness verification on this page has the shape "given in the set, shrink the radius by the distance already travelled", which is the nesting property above. It is recorded here once so that no later proof has to redo the triangle inequality in passing.
Depends on
Used by
- A function continuous on an interval I whose derivative vanishes at every interior point of I is constant on I; consequently two such functions with the same derivative differ by a constant Corollary
- A uniformly continuous real function on a subset D ⊆ ℝ extends uniquely to a uniformly continuous function on the closure of D Corollary
- If f is continuous on an interval I and |f'| ≤ M at every interior point, then |f(x) - f(y)| ≤ M|x-y| for all x,y ∈ I, so f is Lipschitz with constant M and uniformly continuous on I Corollary
- ℚ is F_σ, meager and not G_δ, while the irrationals are G_δ, residual and not F_σ Corollary
- The connected subspaces of ℝ with its usual topology are exactly the order-convex subsets, the published characterisation transported by the identification of the two descriptions of "open in ℝ" Corollary
- [0,1) is neither open nor closed in ℝ Counterexample
- {0} ∪ [1,2] is closed, has an isolated point, and is not perfect Counterexample
- ⋂ₖ (-1/k, 1/k) = {0} is not open Counterexample
- A continuous injection on [0,1] ∪ [2,3] that is not monotone, so the interval hypothesis cannot be dropped from the strict-monotonicity theorem Counterexample
- An upper semicontinuous function on [0,1] that is bounded below and attains no minimum, so the semicontinuous extreme value theorem is genuinely one-sided Counterexample
- f(x) = x on [0,1) with f(1) = 0 is differentiable at every point of (0,1) with f' ≡ 1, yet no c satisfies f(1) - f(0) = f'(c), so continuity on the closed interval cannot be dropped from the mean value theorem Counterexample
- On the domain {0} ∪ [1,2] every real is vacuously a limit at 0 Counterexample
- ℝ is the union of a meager set and a set of measure zero, so smallness of category and smallness of measure are independent notions Counterexample
- The cover {(1/k, 1)} of (0,1) has no finite subcover, so (0,1) is not compact Counterexample
- The Dirichlet function on [0,1] has lower Darboux integral 0 and upper Darboux integral 1, so it is bounded and not Riemann integrable Counterexample
- The function equal to 0 off the origin and to 1 at the origin has limit 0 ≠ 1 there Counterexample
- The identity on [0,1] attains its maximum at 1 and its minimum at 0 with derivative 1 at both, so Fermat's theorem genuinely needs the extremum to be at an interior point Counterexample
- The indicator of ℚ has a limit at no point of ℝ Counterexample
- The indicator of ℚ is continuous at no point of ℝ Counterexample
- The indicator of the Smith-Volterra-Cantor set is discontinuous exactly on a nowhere dense set, and is not Riemann integrable, because that set does not have measure zero Counterexample
- With g ≡ 0 and f equal to 0 off the origin and 1 at it, lim g = 0 and lim_y → 0 f = 0 while f ∘ g ≡ 1 Counterexample
- x ↦ |x| is continuous everywhere and not differentiable at 0: the difference quotient equals 1 on the right and -1 on the left, so the two one-sided limits differ Counterexample
- x ↦ √x on (0,1] is differentiable with unbounded derivative and is not Lipschitz there, so the boundedness hypothesis in the Lipschitz corollary cannot be dropped Counterexample
- ℤ is closed and not compact, and (0,1) is bounded and not compact: neither hypothesis of Heine-Borel can be dropped Counterexample
- ψ(1/x) has no limit at 0: two sequences tending to 0 give values constantly 0 and constantly 1/2 Counterexample
- A real-analytic function on an open subset of ℝ is locally represented by a convergent real power series Definition
- Continuity of f : A → ℝ at a point of A and on A: the ε-δ condition, its agreement with lim_x → c f(x) = f(c) at a limit point, and continuity at an isolated point Definition
- G_δ and F_σ subsets of a topological space, agreeing with the real-line notion Definition
- Interior, closure, boundary and exterior of a subset of ℝ Definition
- Limit point, isolated point, adherent point, derived set, and dense subset of ℝ Definition
- Local (relative) maximum and minimum of f : A → ℝ at a point, the strict forms, and what it means for the point to be interior to A Definition
- Nowhere dense, meager (first category), residual, and second category subsets of ℝ Definition
- Open subset of ℝ (every point has a neighbourhood inside it), closed subset (complement open), and clopen Definition
- Separated sets, disconnection, and connected subset of ℝ Definition
- The derivative f'(c) = lim_x → c f(x) - f(c)/x - c of f : A → ℝ at a point c ∈ A that is a limit point of A, and differentiability on a set Definition
- The order topology of a linearly ordered set, with the open rays as a subbasis; order-convex sets, order-density, the least upper bound property, and linear continua Definition
- The oscillation ω_f(S) = sup{ |f(x) - f(y)| : x, y ∈ S } of f on a set and the oscillation ω_f(c) = inf_δ > 0 ω_f(A ∩ N_δ(c)) at a point, both taken in the extended reals Definition
- The ε-δ limit lim_x → c f(x) = L of f : A → ℝ at a limit point c of A Definition
- Uniform continuity of f : A → ℝ: one δ serving every pair of points of A Definition
- Upper and lower semicontinuity of f : A → ℝ at a point of A and on A Definition
…and 83 more results.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 20 results over 6 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Neighbourhood (mathematics) (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 2 (Def. 2.18(a)) (standard reference, not scraped)
- J. Lebl, Basic Analysis I, §7.1 and §1.4 (standard reference, not scraped)
- J. K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)