In topology, a basis, or base, for a topological space is a collection of open sets from which every open set can be obtained by taking unions. Its members are called basis elements or basic open sets. A basis describes a topology without requiring an explicit list of all its open sets, and provides local criteria for openness and continuity. (leanprover-community.github.io)
Definition and basis axioms
Let be a topological space. A family is a basis for if every is a union of members of . Equivalently, whenever and is open, there exists such that
This condition expresses that basic open sets can fit inside every open neighborhood of each point. (math.toronto.edu)
A basis can also be specified before a topology is chosen. A family of subsets of generates a topology by unions precisely when it satisfies two conditions:
Coverage: every belongs to some .
Local intersection refinement: if , with , there is satisfying
The intersection itself need not be a basis element; it need only be a union of basis elements. (math.toronto.edu)
The generated topology is
Coverage ensures that is open. The empty set is the union of the empty subfamily. Arbitrary unions remain unions of basis elements, while the refinement condition ensures closure under finite intersections. These observations verify the topology axioms. (pi.math.cornell.edu)
Examples
On the real line , all open intervals form a basis for the usual topology. Intervals with rational endpoints also suffice: every point of an open interval lies in a smaller interval with rational endpoints. Thus different bases can generate exactly the same topology. (math.mit.edu)
In a metric space , the open balls
form a basis. In Euclidean space , open boxes provide another basis for the same topology. For example, disks and axis-parallel open squares generate the same topology in the plane because either shape can be fitted around a point inside the other. (pi.math.cornell.edu)
For the discrete topology, the singleton sets form a basis: every subset is a union of singletons. For the indiscrete topology on a nonempty set , the family is a basis. (pi.math.cornell.edu)
Comparing bases and subbases
Suppose and generate topologies and on the same set. Then is finer than , meaning , exactly when every point of every -element lies in a -element contained within it. The topologies agree when this refinement condition holds in both directions. (math.toronto.edu)
A subbasis is a family whose finite intersections form a basis. Consequently, generating a topology from a subbasis generally requires two operations: finite intersections, followed by arbitrary unions. Under the convention that the empty intersection equals , any family of subsets generates a topology this way. This distinction is reflected in the formal definition of topological bases in Mathlib: unions alone must suffice. (math.toronto.edu)
Local bases and countability
A local basis at is a family of neighborhoods of such that every neighborhood of contains one of its members. Unlike a basis for the entire topology, it concerns only one point. Given a global basis , the family
is a local basis at . (math.mit.edu)
A first-countable space has a countable local basis at every point. A second-countable space has a global basis that is a countable set. Second countability implies first countability, but the converse fails: an uncountable discrete space has singleton local bases, yet every global basis must contain every singleton. (math.mit.edu)
Second-countable spaces are separable and Lindelöf. Choosing one point from each nonempty basic open set produces a countable dense set. For an arbitrary open cover, choosing a covering member for each basic set contained in some covering member produces a countable subcover. (math.ucla.edu)
Constructions and applications
If , the family
is a basis for the subspace topology on . If and are bases, the products form a basis for the product topology on . In an arbitrary product, basic sets restrict only finitely many coordinates, leaving all others unrestricted. (pi.math.cornell.edu)
To check that a map is a continuous function, it suffices to verify that is open for every member of a basis for . Every open set in is a union of such members, and inverse images preserve unions. Bases therefore reduce continuity tests to a specified collection of open sets. (leanprover-community.github.io)