Mathlib.Topology.Defs.Basic

Module docstring

{"# 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 @. ","### Predicates on sets ","### Notation for non-standard topologies "}

TopologicalSpace structure

(X : Type u)

Full source

/-- A topology on `X`. -/
@[to_additive existing TopologicalSpace]
class TopologicalSpace (X : Type u) where
  /-- A predicate saying that a set is an open set. Use `IsOpen` in the root namespace instead. -/
  protected IsOpen : Set X → Prop
  /-- The set representing the whole space is an open set.
  Use `isOpen_univ` in the root namespace instead. -/
  protected isOpen_univ : IsOpen univ
  /-- The intersection of two open sets is an open set. Use `IsOpen.inter` instead. -/
  protected isOpen_inter : ∀ s t, IsOpen s → IsOpen t → IsOpen (s ∩ t)
  /-- The union of a family of open sets is an open set.
  Use `isOpen_sUnion` in the root namespace instead. -/
  protected isOpen_sUnion : ∀ s, (∀ t ∈ s, IsOpen t) → IsOpen (⋃₀ s)

Topological space

Informal description

A topology on a type $X$ is a structure consisting of a collection of subsets of $X$ called open sets, satisfying: 1. The whole space $X$ is open. 2. The intersection of any two open sets is open. 3. The union of any family of open sets is open.

IsOpen definition

: Set X → Prop

Full source

/-- `IsOpen s` means that `s` is open in the ambient topological space on `X` -/
def IsOpen : Set X → Prop := TopologicalSpace.IsOpen

Open set in a topological space

Informal description

The predicate `IsOpen s` indicates that a subset $s$ of a topological space $X$ is open, meaning it belongs to the topology of $X$.

isOpen_univ theorem

: IsOpen (univ : Set X)

Full source

@[simp] theorem isOpen_univ : IsOpen (univ : Set X) := TopologicalSpace.isOpen_univ

The universal set is open in any topological space

Informal description

In any topological space $X$, the universal set $\text{univ} = X$ is an open set.

IsOpen.inter theorem

(hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ∩ t)

Full source

theorem IsOpen.inter (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ∩ t) :=
  TopologicalSpace.isOpen_inter s t hs ht

Intersection of Open Sets is Open

Informal description

For any two open sets $s$ and $t$ in a topological space $X$, their intersection $s \cap t$ is also open.

isOpen_sUnion theorem

{s : Set (Set X)} (h : ∀ t ∈ s, IsOpen t) : IsOpen (⋃₀ s)

Full source

theorem isOpen_sUnion {s : Set (Set X)} (h : ∀ t ∈ s, IsOpen t) : IsOpen (⋃₀ s) :=
  TopologicalSpace.isOpen_sUnion s h

Openness of Union of Open Sets in Topological Space

Informal description

For any family of sets $s$ in a topological space $X$, if every set $t \in s$ is open, then the union $\bigcup₀ s$ is also open.

IsClosed structure

(s : Set X)

Full source

/-- A set is closed if its complement is open -/
class IsClosed (s : Set X) : Prop where
  /-- The complement of a closed set is an open set. -/
  isOpen_compl : IsOpen sᶜ

Closed set in a topological space

Informal description

A subset $s$ of a topological space $X$ is called *closed* if its complement $X \setminus s$ is an open set in the topology of $X$.

IsClopen definition

(s : Set X) : Prop

Full source

/-- A set is clopen if it is both closed and open. -/
def IsClopen (s : Set X) : Prop :=
  IsClosedIsClosed s ∧ IsOpen s

Clopen set

Informal description

A subset $s$ of a topological space $X$ is called *clopen* if it is both closed and open, meaning both $s$ and its complement $X \setminus s$ belong to the topology of $X$.

IsLocallyClosed definition

(s : Set X) : Prop

Full source

/--
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`.
-/
def IsLocallyClosed (s : Set X) : Prop := ∃ (U Z : Set X), IsOpen U ∧ IsClosed Z ∧ s = U ∩ Z

Locally closed set

Informal description

A subset $s$ of a topological space $X$ is called *locally closed* if there exist an open set $U$ and a closed set $Z$ in $X$ such that $s = U \cap Z$.

interior definition

(s : Set X) : Set X

Full source

/-- The interior of a set `s` is the largest open subset of `s`. -/
def interior (s : Set X) : Set X :=
  ⋃₀ { t | IsOpen t ∧ t ⊆ s }

Interior of a set in a topological space

Informal description

The interior of a subset $s$ in a topological space $X$ is the union of all open subsets of $X$ that are contained in $s$. In other words, it is the largest open set contained in $s$.

closure definition

(s : Set X) : Set X

Full source

/-- The closure of `s` is the smallest closed set containing `s`. -/
def closure (s : Set X) : Set X :=
  ⋂₀ { t | IsClosed t ∧ s ⊆ t }

Topological closure of a set

Informal description

The closure of a subset $s$ of a topological space $X$ is the smallest closed set containing $s$, defined as the intersection of all closed sets that include $s$. In other words, $\text{closure}(s) = \bigcap \{ t \subseteq X \mid \text{IsClosed}(t) \text{ and } s \subseteq t \}$.

frontier definition

(s : Set X) : Set X

Full source

/-- The frontier of a set is the set of points between the closure and interior. -/
def frontier (s : Set X) : Set X :=
  closureclosure s \ interior s

Topological frontier of a set

Informal description

The frontier of a subset $s$ in a topological space $X$ is the set difference between the closure of $s$ and the interior of $s$, i.e., $\text{frontier}(s) = \text{closure}(s) \setminus \text{interior}(s)$. A point $x$ belongs to the frontier of $s$ if every neighborhood of $x$ contains points both from $s$ and its complement.

coborder definition

(s : Set X) : Set X

Full source

/--
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.
-/
def coborder (s : Set X) : Set X :=
  (closure s \ s)ᶜ

Coborder of a set in a topological space

Informal description

The coborder of a subset $s$ of a topological space $X$ is defined as the complement of the set difference between the closure of $s$ and $s$ itself, i.e., $\text{coborder}(s) = (\text{closure}(s) \setminus s)^c$. This is the largest set in which $s$ is closed, and $s$ is locally closed if and only if $\text{coborder}(s)$ is open.

Dense definition

(s : Set X) : Prop

Full source

/-- A set is dense in a topological space if every point belongs to its closure. -/
def Dense (s : Set X) : Prop :=
  ∀ x, x ∈ closure s

Dense subset of a topological space

Informal description

A subset $s$ of a topological space $X$ is called *dense* if every point $x \in X$ belongs to the closure of $s$. In other words, the closure of $s$ is the entire space $X$.

DenseRange definition

{α : Type*} (f : α → X)

Full source

/-- `f : α → X` has dense range if its range (image) is a dense subset of `X`. -/
def DenseRange {α : Type*} (f : α → X) := Dense (range f)

Function with dense range

Informal description

A function $ f \colon \alpha \to X $ between topological spaces is said to have *dense range* if the range of $ f $, defined as the set $\{ f(x) \mid x \in \alpha \}$, is a dense subset of $ X $. This means that the closure of the range of $ f $ is the entire space $ X $.

Continuous structure

(f : X → Y)

Full source

/-- 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. -/
@[fun_prop]
structure Continuous (f : X → Y) : Prop where
  /-- The preimage of an open set under a continuous function is an open set. Use `IsOpen.preimage`
  instead. -/
  isOpen_preimage : ∀ s, IsOpen s → IsOpen (f ⁻¹' s)

Continuous function

Informal description

A function $f \colon X \to Y$ between topological spaces is called *continuous* if for every open set $U \subseteq Y$, the preimage $f^{-1}(U)$ is open in $X$.

IsOpenMap definition

(f : X → Y) : Prop

Full source

/-- 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`. -/
def IsOpenMap (f : X → Y) : Prop := ∀ U : Set X, IsOpen U → IsOpen (f '' U)

Open map

Informal description

A function $ f \colon X \to Y $ between topological spaces is called an *open map* if for every open subset $ U \subseteq X $, the image $ f(U) $ is open in $ Y $.

IsClosedMap definition

(f : X → Y) : Prop

Full source

/-- 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`. -/
def IsClosedMap (f : X → Y) : Prop := ∀ U : Set X, IsClosed U → IsClosed (f '' U)

Closed map

Informal description

A function $ f \colon X \to Y $ between topological spaces is called a *closed map* if for every closed subset $ U \subseteq X $, the image $ f(U) $ is closed in $ Y $.

IsOpenQuotientMap structure

(f : X → Y)

Full source

/-- 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`.
-/
@[mk_iff]
structure IsOpenQuotientMap (f : X → Y) : Prop where
  /-- An open quotient map is surjective. -/
  surjective : Function.Surjective f
  /-- An open quotient map is continuous. -/
  continuous : Continuous f
  /-- An open quotient map is an open map. -/
  isOpenMap : IsOpenMap f

Open quotient map

Informal description

An open quotient map is a surjective continuous map $ f : X \to Y $ between topological spaces that is also an open map (i.e., the image of any open set in $ X $ is open in $ Y $). This structure captures important examples of quotient maps, such as: - The quotient map from a topological space to its quotient by a group action. - 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. Unlike general quotient maps, the category of open quotient maps is closed under the operation of taking products (via `Prod.map`).

Topology.IsOpen_of definition

: Lean.ParserDescr✝

Full source

/-- Notation for `IsOpen` with respect to a non-standard topology. -/
scoped[Topology] notation (name := IsOpen_of) "IsOpen[" t "]" => @IsOpen _ t

Openness with respect to a custom topology

Informal description

The notation `IsOpen[t]` represents the predicate that a set is open with respect to a non-standard topology `t` on a space. This allows for specifying custom topologies when checking openness of sets without explicitly using the `@` symbol for type annotation.

Topology.IsClosed_of definition

: Lean.ParserDescr✝

Full source

/-- Notation for `IsClosed` with respect to a non-standard topology. -/
scoped[Topology] notation (name := IsClosed_of) "IsClosed[" t "]" => @IsClosed _ t

Closed set predicate with respect to a custom topology

Informal description

The notation `IsClosed[t]` denotes the predicate that a set is closed with respect to a non-standard topology `t`. This allows specifying a custom topology when checking if a set is closed, without explicitly using the `@` symbol for type annotation.

Topology.closure_of definition

: Lean.ParserDescr✝

Full source

/-- Notation for `closure` with respect to a non-standard topology. -/
scoped[Topology] notation (name := closure_of) "closure[" t "]" => @closure _ t

Closure with respect to a non-standard topology

Informal description

The notation `closure[t]` represents the closure of a set with respect to a non-standard topology `t`. Specifically, for a given topology `t` on a space, `closure[t] s` denotes the minimal closed set in the topology `t` that contains the set `s`.

Topology.Continuous_of definition

: Lean.ParserDescr✝

Full source

/-- Notation for `Continuous` with respect to a non-standard topologies. -/
scoped[Topology] notation (name := Continuous_of) "Continuous[" t₁ ", " t₂ "]" =>
  @Continuous _ _ t₁ t₂

Continuity with respect to non-standard topologies

Informal description

The notation `Continuous[t₁, t₂]` denotes the continuity of a function with respect to the topologies `t₁` (on the domain) and `t₂` (on the codomain). A function is continuous in this context if the preimage of any open set in `t₂` is an open set in `t₁`.

BaireSpace structure

(X : Type*) [TopologicalSpace X]

Full source

/-- 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. -/
class BaireSpace (X : Type*) [TopologicalSpace X] : Prop where
  baire_property : ∀ f : ℕ → Set X, (∀ n, IsOpen (f n)) → (∀ n, Dense (f n)) → Dense (⋂ n, f n)

Baire space

Informal description

A topological space $ X $ is called a *Baire space* if it satisfies the Baire property: any countable intersection of open dense subsets of $ X $ is dense in $ X $. This means that for any sequence $ \{U_n\}_{n \in \mathbb{N}} $ of open dense subsets of $ X $, the intersection $ \bigcap_{n \in \mathbb{N}} U_n $ is dense in $ X $.