# Basic definitions about topological spaces #

This file contains definitions about topology that do not require imports other than `Mathlib/Data/Set/Lattice.lean`.

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

source
class TopologicalSpace (X : Type u) :
Type u

A topology on `X`.

- IsOpen : Set X → Prop

  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 #

source
def IsOpen {X : Type u} [TopologicalSpace X] :
Set X → Prop

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

Equations

- IsOpen = TopologicalSpace.IsOpen

Instances For

source
@[simp]
theorem isOpen_univ {X : Type u} [TopologicalSpace X] :
IsOpen Set.univ
source
theorem IsOpen.inter {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsOpen s) (ht : IsOpen t) :
IsOpen (s ∩ t)
source
theorem isOpen_sUnion {X : Type u} [TopologicalSpace X] {s : Set (Set X)} (h : ∀ (t : Set X), t ∈ s → IsOpen t) :
IsOpen (⋃₀ s)
source
class IsClosed {X : Type u} [TopologicalSpace X] (s : Set X) :
Prop

A set is closed if its complement is open

- isOpen_compl : IsOpen s ᶜ

  The complement of a closed set is an open set.

Instances

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

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

Equations

- IsClopen s = (IsClosed s ∧ IsOpen s)

Instances For

source
def IsLocallyClosed {X : Type u} [TopologicalSpace X] (s : Set X) :
Prop

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

Equations

- IsLocallyClosed s = ∃ (U : Set X), ∃ (Z : Set X), IsOpen U ∧ IsClosed Z ∧ s = U ∩ Z

Instances For

source
def interior {X : Type u} [TopologicalSpace X] (s : Set X) :
Set X

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

Equations

- interior s = ⋃₀ {t : Set X | IsOpen t ∧ t ⊆ s}

Instances For

source
def closure {X : Type u} [TopologicalSpace X] (s : Set X) :
Set X

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

Equations

- closure s = ⋂₀ {t : Set X | IsClosed t ∧ s ⊆ t}

Instances For

source
def frontier {X : Type u} [TopologicalSpace X] (s : Set X) :
Set X

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

Equations

- frontier s = closure s \ interior s

Instances For

source
def coborder {X : Type u} [TopologicalSpace X] (s : Set X) :
Set X

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.

Equations

- coborder s = (closure s \ s)ᶜ

Instances For

source
def Dense {X : Type u} [TopologicalSpace X] (s : Set X) :
Prop

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

Equations

- Dense s = ∀ (x : X), x ∈ closure s

Instances For

source
def DenseRange {X : Type u} [TopologicalSpace X] {α : Type u_1} (f : α → X) :
Prop

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

Equations

- DenseRange f = Dense (Set.range f)

Instances For

source
structure Continuous {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) :
Prop

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 s → IsOpen (f ⁻¹' s)

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

Instances For

source
def IsOpenMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) :
Prop

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

- IsOpenMap f = ∀ (U : Set X), IsOpen U → IsOpen (f '' U)

Instances For

source
def IsClosedMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) :
Prop

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

- IsClosedMap f = ∀ (U : Set X), IsClosed U → IsClosed (f '' U)

Instances For

source
structure IsOpenQuotientMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) :
Prop

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

source
theorem isOpenQuotientMap_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) :
IsOpenQuotientMap f ↔ Function.Surjective f ∧ Continuous f ∧ IsOpenMap f

### Notation for non-standard topologies #

source
def Topology.IsOpen_of :
Lean.ParserDescr

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

source
def Topology.IsClosed_of :
Lean.ParserDescr

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

source
def Topology.closure_of :
Lean.ParserDescr

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

source
def Topology.Continuous_of :
Lean.ParserDescr

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

source
class BaireSpace (X : Type u_1) [TopologicalSpace X] :
Prop

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.

- baire_property (f : ℕ → Set X) : (∀ (n : ℕ), IsOpen (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ (n : ℕ), f n)

Instances