# 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 endowing X with a topology. By definition, a topology is a collection of sets called open sets such that

• isOpen_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 that s is an open set, same as TopologicalSpace.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 set s is the maximal open set that is included in s.

• closure s: the closure of a set s is the minimal closed set that includes s.

• frontier s: the frontier of a set is the set difference closure s \ interior s. A point x belongs to frontier s, if any neighborhood of x contains points both from s and sᶜ.

• 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, if Set.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 @.

class TopologicalSpace (X : Type u) :

A topology on X.

• IsOpen : Set XProp

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),

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)

The union of a family of open sets is an open set. Use isOpen_sUnion in the root namespace instead.

Instances
theorem TopologicalSpace.isOpen_univ {X : Type u} [self : ] :

The set representing the whole space is an open set. Use isOpen_univ in the root namespace instead.

theorem TopologicalSpace.isOpen_inter {X : Type u} [self : ] (s : Set X) (t : Set X) :

The intersection of two open sets is an open set. Use IsOpen.inter instead.

theorem TopologicalSpace.isOpen_sUnion {X : Type u} [self : ] (s : Set (Set X)) :
(∀ (t : Set X), t s)

The union of a family of open sets is an open set. Use isOpen_sUnion in the root namespace instead.

### Predicates on sets #

def IsOpen {X : Type u} [] :
Set XProp

IsOpen s means that s is open in the ambient topological space on X

Equations
• IsOpen = TopologicalSpace.IsOpen
Instances For
@[simp]
theorem isOpen_univ {X : Type u} [] :
IsOpen Set.univ
theorem IsOpen.inter {X : Type u} [] {s : Set X} {t : Set X} (hs : ) (ht : ) :
IsOpen (s t)
theorem isOpen_sUnion {X : Type u} [] {s : Set (Set X)} (h : ∀ (t : Set X), t s) :
class IsClosed {X : Type u} [] (s : Set X) :

A set is closed if its complement is open

• isOpen_compl :

The complement of a closed set is an open set.

Instances
theorem IsClosed.isOpen_compl {X : Type u} [] {s : Set X} [self : ] :

The complement of a closed set is an open set.

def IsClopen {X : Type u} [] (s : Set X) :

A set is clopen if it is both closed and open.

Equations
Instances For
def interior {X : Type u} [] (s : Set X) :
Set X

The interior of a set s is the largest open subset of s.

Equations
Instances For
def closure {X : Type u} [] (s : Set X) :
Set X

The closure of s is the smallest closed set containing s.

Equations
Instances For
def frontier {X : Type u} [] (s : Set X) :
Set X

The frontier of a set is the set of points between the closure and interior.

Equations
Instances For
def Dense {X : Type u} [] (s : Set X) :

A set is dense in a topological space if every point belongs to its closure.

Equations
• = ∀ (x : X), x
Instances For
def DenseRange {X : Type u} [] {α : Type u_1} (f : αX) :

f : α → X has dense range if its range (image) is a dense subset of X.

Equations
Instances For
structure Continuous {X : Type u} {Y : Type v} [] [] (f : XY) :

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.

• isOpen_preimage : ∀ (s : Set Y), IsOpen (f ⁻¹' s)

The preimage of an open set under a continuous function is an open set. Use IsOpen.preimage instead.

Instances For
theorem Continuous.isOpen_preimage {X : Type u} {Y : Type v} [] [] {f : XY} (self : ) (s : Set Y) :
IsOpen (f ⁻¹' s)

The preimage of an open set under a continuous function is an open set. Use IsOpen.preimage instead.

def IsOpenMap {X : Type u} {Y : Type v} [] [] (f : XY) :

A map f : X → Y is said to be an open map, if the image of any open U : Set X is open in Y.

Equations
Instances For
def IsClosedMap {X : Type u} {Y : Type v} [] [] (f : XY) :

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.

Equations
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
class BaireSpace (X : Type u_1) [] :

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.

Instances
theorem BaireSpace.baire_property {X : Type u_1} [] [self : ] (f : Set X) :
(∀ (n : ), IsOpen (f n))(∀ (n : ), Dense (f n))Dense (⋂ (n : ), f n)