# 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 `@`

.

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

The set representing the whole space is an open set.
Use `isOpen_univ`

in the root namespace instead.

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

instead.

The union of a family of open sets is an open set.
Use `isOpen_sUnion`

in the root namespace instead.

### Predicates on sets #

The complement of a closed set is an open set.

`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

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

instead.

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 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.