Documentation

Mathlib.Topology.Defs.Basic

Basic definitions about topological spaces #

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

Main definitions #

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

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
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
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
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
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
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
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
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
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
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
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
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 spaace to its separation quotient.

Contrary to general quotient maps, the category of open quotient maps is closed under Prod.map.

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

Instances