Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-03 (gpt-5.6-sol-codex-subscription)
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.

Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open

Definition

Let (X,T) be a topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison) and let x∈X.

A set N⊆X is a neighbourhood of x if there is an open U∈T with x∈U⊆N. The family of all neighbourhoods of x is written N(x) and called the neighbourhood filter at x. A neighbourhood that is itself open is an open neighbourhood.

Convention, and it is a live fork: in this library a neighbourhood need not be open. The competing convention, used by Munkres among others, defines a neighbourhood of x to be an open set containing x. Both are in current use; this library follows the one above and writes "open neighbourhood" in full whenever openness is wanted, so that no statement here depends on which convention a reader brings.

A family Bx⊆N(x) is a neighbourhood base at x if every neighbourhood of x contains a member of Bx: for every N∈N(x) there is B∈Bx with B⊆N.

Four immediate consequences, established here because they are used constantly.

  1. X is a neighbourhood of each of its points, since x∈X⊆X and X is open by (T1); so N(x)≠∅ and every point has at least one neighbourhood base, namely N(x) itself.
  2. A superset of a neighbourhood of x is a neighbourhood of x: if x∈U⊆N⊆M with U open then x∈U⊆M.
  3. The intersection of two neighbourhoods of x is a neighbourhood of x: if x∈U⊆N and x∈V⊆M with U,V open, then U∩V is open by (T3) and x∈U∩V⊆N∩M. By iteration the same holds for any intersection of finitely many neighbourhoods of x.
  4. A set is open exactly when it is a neighbourhood of each of its points. If U is open and x∈U then x∈U⊆U. Conversely, if N is a neighbourhood of each of its points, choose for each x∈N an open Ux with x∈Ux⊆N; then N=⋃x∈NUx is open by (T2). No choice principle is involved: Ux may be taken to be the union of all open subsets of N containing x, which is determined by x and N, and is open by (T2).

Basic sets give neighbourhood bases. If B is a basis for T (Basis and subbasis for a topology, and the topology generated by a family of sets) then Bx:={ B∈B:x∈B } is a neighbourhood base at x consisting of open sets. Each such B is open and contains x, hence is a neighbourhood of x; and if N∈N(x), fix open U with x∈U⊆N and then B∈B with x∈B⊆U, which gives B∈Bx with B⊆N. A member of Bx is called a basic neighbourhood of x.

Remarks

  • The convention costs nothing and buys one thing. Every statement of the form "for every neighbourhood N of x ... " whose predicate is preserved when N is enlarged is equivalent to the statement with N restricted to open neighbourhoods: every neighbourhood contains an open one, and the predicate then passes to the larger set. Eventual-membership and the usual local-existence tests have this form; an arbitrary predicate need not. What the wider notion buys is that N(x) is a filter on X in the sense of Filter on a set: consequence 1 is (F1), consequence 3 is (F3), consequence 2 is (F4), and (F2) holds because x∈U⊆∅ is impossible, so ∅ is a neighbourhood of no point. Under the narrower convention the family of open sets containing x fails (F4) as soon as some non-open set contains an open set around x, so the name "neighbourhood filter" would not be available.

  • A neighbourhood base is not required to be closed under intersection, and the bases used below usually are not; what is required is only that its members be cofinal downwards among neighbourhoods.

Depends on

Used by

…and 31 more results.

Dependency tree · two levels

3 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources