Basic definitions about topological spaces #
This file contains definitions about topology that do not require imports
other than Mathlib.Data.Set.Lattice
.
Main definitions #
TopologicalSpace X
: a typeclass endowingX
with a topology. By definition, a topology is a collection of sets called open sets such thatisOpen_univ
: the whole space is open;IsOpen.inter
: the intersection of two open sets is an open set;isOpen_sUnion
: the union of a family of open sets is an open set.
IsOpen s
: predicate saying thats
is an open set, same asTopologicalSpace.IsOpen
.IsClosed s
: a set is called closed, if its complement is an open set. For technical reasons, this is a typeclass.IsClopen s
: a set is clopen if it is both closed and open.interior s
: the interior of a sets
is the maximal open set that is included ins
.closure s
: the closure of a sets
is the minimal closed set that includess
.frontier s
: the frontier of a set is the set differenceclosure s \ interior s
. A pointx
belongs tofrontier s
, if any neighborhood ofx
contains points both froms
andsᶜ
.Dense s
: a set is dense if its closure is the whole space. We define it as∀ x, x ∈ closure s
so that one can write(h : Dense s) x
.DenseRange f
: a function has dense range, ifSet.range f
is a dense set.Continuous f
: a map is continuous, if the preimage of any open set is an open set.IsOpenMap f
: a map is an open map, if the image of any open set is an open set.IsClosedMap f
: a map is a closed map, if the image of any closed set is a closed set.
** Notation
We introduce notation IsOpen[t]
, IsClosed[t]
, closure[t]
, Continuous[t₁, t₂]
that allow passing custom topologies to these predicates and functions without using @
.
A topology on X
.
A predicate saying that a set is an open set. Use
IsOpen
in the root namespace instead.- isOpen_univ : TopologicalSpace.IsOpen Set.univ
The set representing the whole space is an open set. Use
isOpen_univ
in the root namespace instead. - isOpen_inter (s t : Set X) : TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
The intersection of two open sets is an open set. Use
IsOpen.inter
instead. - isOpen_sUnion (s : Set (Set X)) : (∀ (t : Set X), t ∈ s → TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
The union of a family of open sets is an open set. Use
isOpen_sUnion
in the root namespace instead.
Instances
Predicates on sets #
A set is locally closed if it is the intersection of some open set and some closed set.
Also see isLocallyClosed_tfae
and other lemmas in Mathlib/Topology/LocallyClosed.lean
.
Instances For
The coborder is defined as the complement of closure s \ s
,
or the union of s
and the complement of ∂(s)
.
This is the largest set in which s
is closed, and s
is locally closed if and only if
coborder s
is open.
This is unnamed in the literature, and this name is due to the fact that coborder s = (border sᶜ)ᶜ
where border s = s \ interior s
is the border in the sense of Hausdorff.
Instances For
f : α → X
has dense range if its range (image) is a dense subset of X
.
Equations
- DenseRange f = Dense (Set.range f)
Instances For
A function between topological spaces is continuous if the preimage of every open set is open. Registered as a structure to make sure it is not unfolded by Lean.
The preimage of an open set under a continuous function is an open set. Use
IsOpen.preimage
instead.
Instances For
A map f : X → Y
is said to be a closed map,
if the image of any closed U : Set X
is closed in Y
.
Instances For
An open quotient map is an open map f : X → Y
which is both an open map and a quotient map.
Equivalently, it is a surjective continuous open map.
We use the latter characterization as a definition.
Many important quotient maps are open quotient maps, including
- the quotient map from a topological space to its quotient by the action of a group;
- the quotient map from a topological group to its quotient by a normal subgroup;
- the quotient map from a topological spaace to its separation quotient.
Contrary to general quotient maps,
the category of open quotient maps is closed under Prod.map
.
- surjective : Function.Surjective f
An open quotient map is surjective.
- continuous : Continuous f
An open quotient map is continuous.
- isOpenMap : IsOpenMap f
An open quotient map is an open map.
Instances For
Notation for non-standard topologies #
Notation for IsOpen
with respect to a non-standard topology.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Notation for IsClosed
with respect to a non-standard topology.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Notation for closure
with respect to a non-standard topology.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Notation for Continuous
with respect to a non-standard topologies.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The property BaireSpace α
means that the topological space α
has the Baire property:
any countable intersection of open dense subsets is dense.
Formulated here when the source space is ℕ.
Use dense_iInter_of_isOpen
which works for any countable index type instead.