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 that 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 #
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
Notation for nonstandard topologies #
Notation for IsOpen
with respect to a nonstandard topology.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Notation for IsClosed
with respect to a nonstandard topology.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Notation for closure
with respect to a nonstandard topology.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Notation for Continuous
with respect to a nonstandard 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.