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} [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 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 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)

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} [TopologicalSpace X] [self : BaireSpace X] (f : ℕ → Set X) : (∀ (n : ℕ), IsOpen (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ (n : ℕ), f n)