Documentation

Marginis.CoquandMaiettiPalmgren2019

Preface to the special issue for The Fifth Workshop on Formal Topology #

by THIERRY COQUAND MARIA EMILIA MAIETTI ERIK PALMGREN

The paper introduces Formal Topology, which is a constructive approach to pointfree topology. Here we instead look at topologies with points, over finite sets and show:

theorem uniqueTopFin0 (σ : TopologicalSpace (Fin 0)) (τ : TopologicalSpace (Fin 0)) :
TopologicalSpace.IsOpen = TopologicalSpace.IsOpen

There is only one topology on Fin 0.

theorem uniqueTopFin1 (σ : TopologicalSpace (Fin 1)) (τ : TopologicalSpace (Fin 1)) :
TopologicalSpace.IsOpen = TopologicalSpace.IsOpen

There is only one topology on Fin 0.

theorem nonUniqueTopFin2 :
∃ (σ : TopologicalSpace (Fin 2)) (τ : TopologicalSpace (Fin 2)), TopologicalSpace.IsOpen TopologicalSpace.IsOpen

There are two distinct topologies on Fin 2.

def mytop (z : Fin 2) :

Here are two more topologies on Fin 2. In fact a topology on Fin 2 must contain Set.univ and , and then there are four possibilities depending on which of {0}, {1} are included.

Equations
  • mytop z = { IsOpen := fun (S : Set (Fin 2)) => S = S = Set.univ S = {z}, isOpen_univ := , isOpen_inter := , isOpen_sUnion := }
Instances For
    def myequiv :
    Fin 2 Fin 2

    We can show that the latter two topologies are homeomorphic.

    Equations
    Instances For
      Equations
      Instances For