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

theorem TopologicalSpace.isOpen_univ {X : Type u} [self : TopologicalSpace X] : TopologicalSpace.IsOpen Set.univ

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 : TopologicalSpace X] (s : Set X) (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.

theorem TopologicalSpace.isOpen_sUnion {X : Type u} [self : TopologicalSpace X] (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.

Predicates on sets

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

@[simp]

theorem isOpen_univ {X : Type u} [TopologicalSpace X] : IsOpen Set.univ

theorem IsOpen.inter {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ∩ t)

theorem isOpen_sUnion {X : Type u} [TopologicalSpace X] {s : Set (Set X)} (h : ∀ (t : Set X), t ∈ s → IsOpen t) : IsOpen (⋃₀ s)

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.

theorem IsClosed.isOpen_compl {X : Type u} : ∀ {inst : TopologicalSpace X} {s : Set X} [self : IsClosed s], IsOpen sᶜ

The complement of a closed set is an open set.

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)

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.

Equations

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

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}

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}

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

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

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

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)

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.

theorem Continuous.isOpen_preimage {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (self : Continuous f) (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.

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)

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)

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

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.

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

theorem IsOpenQuotientMap.surjective {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (self : IsOpenQuotientMap f) : Function.Surjective f

An open quotient map is surjective.

theorem IsOpenQuotientMap.continuous {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (self : IsOpenQuotientMap f) : Continuous f

An open quotient map is continuous.

theorem IsOpenQuotientMap.isOpenMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (self : IsOpenQuotientMap f) : IsOpenMap f

An open quotient map is an open map.

Notation for non-standard topologies

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.

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.

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.

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.

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)

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