Modèle décidable de la Topologie générale

GENERAL TOPOLOGY on Distributive Set Theory


This software is provided “as is” and is without warranty of any kind. The authors of this software do not warrant, guarantee or make any representations regarding the use or results of use of this software in terms of reliability, accuracy or fitness for purpose. You assume the entire risk of direct or indirect, consequential or inconsequential results from the correct or incorrect usage of this software even if the authors have been informed of the possibilities of such damage. Neither the authors, the Université Savoie Mont Blanc, nor anybody connected to this software in any way can assume any responsibility.

General Information

Topology_on_DST_structurev1.v is a Coq library created by R. Dapoigny and P. Barlatier whose purpose is to propose a decidable and consistent structure of general topology . To reach that objective, the developed structure relies again on the Distributive Set Theory (DST for short) expressed in Dependent Type Theory and based on characteristic functions to formulate appropriate definitions. Then, using Clay’s single axiom for partial order, and adding the two basic axioms of general topology (i.e., union and intersection of open sets) we demonstrate that this axiom is provable assuming set inclusion as partial order and a universe of existing regular open sets.  As a result, the developed library is a theoretical construct depending on few axioms and on a set of definitions.


  • Coq (> v8.9)