Module mathcomp.analysis.topology_theory.topology_structure

# Basic topological notions This file develops tools for the manipulation of basic topological notions. The development of topological notions builds on "filtered types" by extending the hierarchy. ## Mathematical structures ### Topology ``` topologicalType == interface type for topological space structure the HB class is Topological. subTopologicalType S == join of SubNbhs and Topological where S has pred V with V a topologicalType the HB class is SubTopological. ptopologicalType == a pointed topologicalType open == set of open sets closed == set of closed sets clopen U == U is both open and closed open_nbhs p == set of open neighbourhoods of p basis B == a family of open sets that converges to each point second_countable T == T has a countable basis [locally P] := forall a, A a -> G (within A (nbhs x)) if P is convertible to G (globally A) U° == all of the points which are locally in U, i.e., the largest open set contained in U This is a notation for `interior U`. closure U == the smallest closed set containing U regopen U == U is regular open, i.e., equal to the interior of its closure regclosed U == U is regular closed, i.e., equal to the closure of its interior open_of_nbhs B == the open sets induced by neighborhoods nbhs_of_open B == the neighborhoods induced by open sets x^' == set of neighbourhoods of x where x is excluded (a "deleted neighborhood") limit_point E == the set of limit points of E isolated A == the set of isolated points of A dense S == the set (S : set T) is dense in T, with T of type topologicalType continuousType == type of continuous functions The HB structures is Continuous. mkcts f_cts == object of type continuousType corresponding to the function f (f_cts : continuous f) ``` ### Factories ``` Nbhs_isNbhsTopological == factory for a topology defined by a filter It builds the mixin for a topological space from the properties of nbhs and hence assumes that the carrier is a filterType. isOpenTopological == factory for a topology defined by open sets It builds the mixin for a topological space from the properties of open sets, nbhs_of_open must be used to declare a filterType. isBaseTopological == factory for a topology defined by a base of open sets It builds the mixin for a topological space from the properties of a base of open sets; the type of indices must be a pointedType isSubBaseTopological == factory for a topology defined by a subbase of open sets It builds the mixin for a topological space from a subbase of open sets b indexed on domain D ```