The main definition is the type class topological space α which endows a type α with a topology. Then set α gets predicates is_open, is_closed and functions interior, closure and frontier. Each point x of α gets a neighborhood filter nhds x.
This file also defines locally finite families of subsets of α.
For topological spaces α and β, a function f : α → β and a point a : α, continuous_at f a means f is continuous at a, and global continuity is continuous f. There is also a version of continuity pcontinuous for partially defined functions.
Topology in mathlib heavily uses filters (even more than in Bourbaki). See explanations in docs/theories/topology.md.
topological space, interior, closure, frontier, neighborhood, continuity, continuous function
A topology on α.
is_open s means that s is open in the ambient topological space on α
A set is closed if its complement is open
The interior of a set s is the largest open subset of s.
The closure of s is the smallest closed set containing s.
The frontier of a set is the set of points between the closure and interior.
neighbourhood filter
x belongs to the closure of s if and only if some ultrafilter supported on s converges to x.
If f is a filter, then lim f is a limit of the filter, if it exists.
A family of sets in set α is locally finite if at every point x:α, there is a neighborhood of x which meets only finitely many sets in the family
A function between topological spaces is continuous if the preimage of every open set is open.
A function between topological spaces is continuous at a point x₀ if f x tends to f x₀ when x tends to x₀.
Continuity of a partial function